src/Pure/Isar/toplevel.ML
changeset 40960 9e54eb514a46
parent 40132 7ee65dbffa31
child 41536 47fef6afe756
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sat Dec 04 18:41:12 2010 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Dec 04 21:26:55 2010 +0100
     1.3 @@ -486,12 +486,13 @@
     1.4      let
     1.5        val prf = init int gthy;
     1.6        val skip = ! skip_proofs;
     1.7 -      val schematic = Proof.schematic_goal prf;
     1.8 +      val (is_goal, no_skip) =
     1.9 +        (true, Proof.schematic_goal prf) handle ERROR _ => (false, true);
    1.10      in
    1.11 -      if skip andalso schematic then
    1.12 +      if is_goal andalso skip andalso no_skip then
    1.13          warning "Cannot skip proof of schematic goal statement"
    1.14        else ();
    1.15 -      if skip andalso not schematic then
    1.16 +      if skip andalso not no_skip then
    1.17          SkipProof (0, (finish gthy (Proof.global_skip_proof int prf), gthy))
    1.18        else Proof (Proof_Node.init prf, (finish gthy, gthy))
    1.19      end