# HG changeset patch
# User wenzelm
# Date 1283721976 -7200
# Node ID 53886463f559fcedb8e2b85519f7c42d3e3c8757
# Parent  ccb53edd59f0fd78f91a5b786f261081d26b3807
use setmp_noncritical for sequential Pure bootstrap;

diff -r ccb53edd59f0 -r 53886463f559 src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Sun Sep 05 23:16:21 2010 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Sun Sep 05 23:26:16 2010 +0200
@@ -78,7 +78,7 @@
 
 (* 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);
@@ -167,7 +167,7 @@
   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") (),
diff -r ccb53edd59f0 -r 53886463f559 src/Tools/auto_solve.ML
--- a/src/Tools/auto_solve.ML	Sun Sep 05 23:16:21 2010 +0200
+++ b/src/Tools/auto_solve.ML	Sun Sep 05 23:26:16 2010 +0200
@@ -33,7 +33,7 @@
 
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_tracing
-  (setmp_CRITICAL auto true (fn () =>
+  (setmp_noncritical auto true (fn () =>
     Preferences.bool_pref auto
       "auto-solve"
       "Try to solve newly declared lemmas with existing theorems.") ());
diff -r ccb53edd59f0 -r 53886463f559 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Sun Sep 05 23:16:21 2010 +0200
+++ b/src/Tools/quickcheck.ML	Sun Sep 05 23:26:16 2010 +0200
@@ -40,7 +40,7 @@
 
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_tracing
-  (setmp_CRITICAL auto true (fn () =>
+  (setmp_noncritical auto true (fn () =>
     Preferences.bool_pref auto
       "auto-quickcheck"
       "Whether to run Quickcheck automatically.") ());