# HG changeset patch
# User wenzelm
# Date 1152031199 -7200
# Node ID a4332e71c1deb5abb675364a9c872ec6c87d3780
# Parent  7f841a2b431ccdbe5ff71badb7cf0257e7c39114
skip_proofs: do not skip proofs of schematic goals (warning);

diff -r 7f841a2b431c -r a4332e71c1de src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Jul 04 18:39:58 2006 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jul 04 18:39:59 2006 +0200
@@ -464,9 +464,17 @@
 
 fun theory_to_proof f = app_current (fn int =>
   (fn Theory (thy, _) =>
-    if ! skip_proofs then
-      SkipProof ((History.init (undo_limit int) 0, #2 (Proof.global_skip_proof int (f thy))), thy)
-    else Proof (ProofHistory.init (undo_limit int) (f thy), thy)
+    let
+      val prf = f thy;
+      val schematic = Proof.schematic_goal prf;
+    in
+      if ! skip_proofs andalso schematic then
+        warning "Cannot skip proof of schematic goal statement"
+      else ();
+      if ! skip_proofs andalso not schematic then
+        SkipProof ((History.init (undo_limit int) 0, #2 (Proof.global_skip_proof int prf)), thy)
+      else Proof (ProofHistory.init (undo_limit int) prf, thy)
+    end
   | _ => raise UNDEF));
 
 fun proofs' f = map_current (fn int =>