diff -r dd8208a3655a -r 93b8e30a5d1f src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Thu Nov 03 23:32:31 2011 +0100
+++ b/src/Pure/Isar/proof_context.ML	Thu Nov 03 23:55:53 2011 +0100
@@ -793,10 +793,9 @@
     val (args, ctxt') = prep_propp mode parse_prop raw_args ctxt;
     val binds = flat (flat (map (map (simult_matches ctxt')) args));
     val propss = map (map #1) args;
-
-    (*generalize result: context evaluated now, binds added later*)
-    val gen = Variable.exportT_terms ctxt' ctxt;
-    fun gen_binds c = c |> bind_terms (map #1 binds ~~ map SOME (gen (map #2 binds)));
+    fun gen_binds ctxt0 = ctxt0
+      |> bind_terms (map #1 binds ~~
+          map (SOME o Term.close_schematic_term) (Variable.export_terms ctxt' ctxt0 (map #2 binds)));
   in ((propss, gen_binds), ctxt' |> bind_terms (map (apsnd SOME) binds)) end;
 
 in