src/Pure/Tools/proof_general_pure.ML
changeset 54717 42c209a6c225
parent 53403 c09f4005d6bd
child 56265 785569927666
--- a/src/Pure/Tools/proof_general_pure.ML	Wed Dec 11 00:17:09 2013 +0000
+++ b/src/Pure/Tools/proof_general_pure.ML	Wed Dec 11 18:02:22 2013 +0100
@@ -161,9 +161,11 @@
     "Record full proof objects internally";
 
 val _ =
-  ProofGeneral.preference_int ProofGeneral.category_proof
+  ProofGeneral.preference ProofGeneral.category_proof
     NONE
-    Multithreading.max_threads
+    (Markup.print_int o Multithreading.max_threads_value)
+    (Multithreading.max_threads_update o Markup.parse_int)
+    ProofGeneral.pgipint
     "max-threads"
     "Maximum number of threads";
 
@@ -172,7 +174,7 @@
     NONE
     (fn () => Markup.print_bool (! Goal.parallel_proofs >= 1))
     (fn s => Goal.parallel_proofs := (if Markup.parse_bool s then 1 else 0))
-    ProofGeneral.pgipbool
+    ProofGeneral.pgipint
     "parallel-proofs"
     "Check proofs in parallel";