--- a/src/Pure/Tools/proof_general_pure.ML Wed May 15 20:39:25 2013 +0200
+++ b/src/Pure/Tools/proof_general_pure.ML Wed May 15 20:45:27 2013 +0200
@@ -106,13 +106,8 @@
"Whether to enable debugging";
val _ =
- ProofGeneral.preference_raw ProofGeneral.category_tracing
- (fn () => Markup.print_bool (print_mode_active ProofGeneral.thm_depsN))
- (fn s =>
- if Markup.parse_bool s
- then Unsynchronized.change print_mode (insert (op =) ProofGeneral.thm_depsN)
- else Unsynchronized.change print_mode (remove (op =) ProofGeneral.thm_depsN))
- ProofGeneral.pgipbool
+ ProofGeneral.preference_bool ProofGeneral.category_tracing
+ ProofGeneral.thm_deps
"theorem-dependencies"
"Track theorem dependencies within Proof General";