src/Pure/ProofGeneral/preferences.ML

   generic_pref PgipTypes.bool_to_pgstring PgipTypes.read_pgipbool PgipTypes.Pgipbool;
 
 
 (* preferences of Pure *)
 
-val proof_pref = setmp_CRITICAL Proofterm.proofs 1 (fn () =>
+val proof_pref = setmp_noncritical Proofterm.proofs 1 (fn () =>
   let
     fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2);
     fun set s = Proofterm.proofs := (if PgipTypes.read_pgipbool s then 2 else 1);
   in mkpref get set PgipTypes.Pgipbool "full-proofs" "Record full proof objects internally" end) ();
 

     "debugging"
     "Whether to enable debugging.",
   thm_deps_pref];
 
 val proof_preferences =
- [setmp_CRITICAL quick_and_dirty true (fn () =>
+ [setmp_noncritical quick_and_dirty true (fn () =>
     bool_pref quick_and_dirty
       "quick-and-dirty"
       "Take a few short cuts") (),
   bool_pref Toplevel.skip_proofs
     "skip-proofs"