more thorough treatment of build prefs, guarded by system option "build_through": avoid accidental rebuild of HOL etc.;