more uniform notion of disabled proofs -- NB: historic meaning of 1 for recording theorems is already included in 0;

--- a/src/Pure/Tools/proof_general_pure.ML	Sun Jun 30 12:30:02 2013 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML	Sun Jun 30 12:39:39 2013 +0200
@@ -153,7 +153,7 @@
   ProofGeneral.preference ProofGeneral.category_proof
     NONE
     (Markup.print_bool o Proofterm.proofs_enabled)
-    (fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 1))
+    (fn s => Proofterm.proofs := (if Markup.parse_bool s then 2 else 0))
     ProofGeneral.pgipbool
     "full-proofs"
     "Record full proof objects internally";