skip_proofs: do not skip proofs of schematic goals (warning);

--- 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 =>