diff -r c486ac962b89 -r df8fc0567a3d src/Pure/Isar/outer_syntax.ML
--- 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;