src/Pure/goal.ML
changeset 52710 52790e3961fe
parent 52696 38466f4f3483
child 52732 b4da1f2ec73f
--- a/src/Pure/goal.ML	Fri Jul 19 17:35:12 2013 +0200
+++ b/src/Pure/goal.ML	Fri Jul 19 17:58:57 2013 +0200
@@ -6,7 +6,6 @@
 
 signature BASIC_GOAL =
 sig
-  val skip_proofs: bool Unsynchronized.ref
   val parallel_proofs: int Unsynchronized.ref
   val SELECT_GOAL: tactic -> int -> tactic
   val PREFER_GOAL: tactic -> int -> tactic
@@ -200,10 +199,8 @@
 
 (* scheduling parameters *)
 
-val skip_proofs = Unsynchronized.ref false;
-
 fun skip_proofs_enabled () =
-  let val skip = ! skip_proofs in
+  let val skip = Options.default_bool "skip_proofs" in
     if Proofterm.proofs_enabled () andalso skip then
       (warning "Proof terms enabled -- cannot skip proofs"; false)
     else skip