# HG changeset patch
# User wenzelm
# Date 1414484407 -3600
# Node ID 492b64eccd104a011ea0ee8715cf7bbf9727bd05
# Parent  e1a6a71b741dc70f9897de40e21d2dbf1324ece9
tuned;

diff -r e1a6a71b741d -r 492b64eccd10 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Mon Oct 27 20:31:51 2014 +0100
+++ b/src/Pure/Isar/toplevel.ML	Tue Oct 28 09:20:07 2014 +0100
@@ -473,14 +473,13 @@
     let
       val (finish, prf) = init int gthy;
       val skip = Goal.skip_proofs_enabled ();
-      val (is_goal, no_skip) =
-        (true, Proof.schematic_goal prf) handle ERROR _ => (false, true);
+      val schematic_goal = try Proof.schematic_goal prf;
       val _ =
-        if is_goal andalso skip andalso no_skip then
+        if skip andalso schematic_goal = SOME true then
           warning "Cannot skip proof of schematic goal statement"
         else ();
     in
-      if skip andalso not no_skip then
+      if skip andalso schematic_goal = SOME false then
         Skipped_Proof (0, (finish (Proof.global_skip_proof true prf), gthy))
       else Proof (Proof_Node.init prf, (finish, gthy))
     end