--- a/src/Pure/Isar/outer_syntax.ML Tue Apr 10 20:42:17 2012 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Tue Apr 10 21:31:05 2012 +0200
@@ -296,7 +296,8 @@
val (tr, proper_head) = read head |>> Toplevel.modify_init init;
val proof_trs = map read proof |> filter #2 |> map #1;
in
- if proper_head andalso proper_proof then [(tr, proof_trs)]
+ if proper_head andalso proper_proof andalso
+ not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
end;