--- a/src/Pure/ProofGeneral/preferences.ML Thu Feb 03 18:57:42 2011 +0100
+++ b/src/Pure/ProofGeneral/preferences.ML Thu Feb 03 19:21:12 2011 +0100
@@ -84,7 +84,7 @@
val proof_pref = Unsynchronized.setmp Proofterm.proofs 1 (fn () =>
let
- fun get () = PgipTypes.bool_to_pgstring (! Proofterm.proofs >= 2);
+ fun get () = PgipTypes.bool_to_pgstring (Proofterm.proofs_enabled ());
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) ();