src/Pure/Isar/toplevel.ML
changeset 51553 63327f679cff
parent 51423 e5f9a6d9ca82
child 51555 6aa64925db77
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Mar 27 14:50:30 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Mar 27 16:38:25 2013 +0100
     1.3 @@ -29,7 +29,6 @@
     1.4    val interact: bool Unsynchronized.ref
     1.5    val timing: bool Unsynchronized.ref
     1.6    val profiling: int Unsynchronized.ref
     1.7 -  val skip_proofs: bool Unsynchronized.ref
     1.8    val program: (unit -> 'a) -> 'a
     1.9    val thread: bool -> (unit -> unit) -> Thread.thread
    1.10    type transition
    1.11 @@ -229,7 +228,6 @@
    1.12  val interact = Unsynchronized.ref false;
    1.13  val timing = Unsynchronized.ref false;
    1.14  val profiling = Unsynchronized.ref 0;
    1.15 -val skip_proofs = Unsynchronized.ref false;
    1.16  
    1.17  fun program body =
    1.18   (body
    1.19 @@ -522,7 +520,7 @@
    1.20    (fn Theory (gthy, _) =>
    1.21      let
    1.22        val (finish, prf) = init int gthy;
    1.23 -      val skip = ! skip_proofs;
    1.24 +      val skip = ! Goal.skip_proofs;
    1.25        val (is_goal, no_skip) =
    1.26          (true, Proof.schematic_goal prf) handle ERROR _ => (false, true);
    1.27        val _ =
    1.28 @@ -531,7 +529,7 @@
    1.29          else ();
    1.30      in
    1.31        if skip andalso not no_skip then
    1.32 -        SkipProof (0, (finish (Proof.global_skip_proof int prf), gthy))
    1.33 +        SkipProof (0, (finish (Proof.global_skip_proof true prf), gthy))
    1.34        else Proof (Proof_Node.init prf, (finish, gthy))
    1.35      end
    1.36    | _ => raise UNDEF));