clarified default for Proofterm.proofs, according to etc/options and innermost setmp;
authorwenzelm
Wed, 15 May 2013 20:28:43 +0200
changeset 52008 bdb82afdcb92
parent 52007 0b1183012a3c
child 52009 3b18ef9df768
clarified default for Proofterm.proofs, according to etc/options and innermost setmp;
src/Pure/ProofGeneral/proof_general_pure.ML
--- a/src/Pure/ProofGeneral/proof_general_pure.ML	Wed May 15 20:22:46 2013 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pure.ML	Wed May 15 20:28:43 2013 +0200
@@ -133,7 +133,7 @@
     "Skip over proofs";
 
 val _ =
-  Unsynchronized.setmp Proofterm.proofs 0 (fn () =>
+  Unsynchronized.setmp Proofterm.proofs 1 (fn () =>
     ProofGeneral.preference_raw ProofGeneral.category_proof
       (Markup.print_bool o Proofterm.proofs_enabled)
       (fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 1))