diff -r c755dfd02509 -r 71667e5c2ff8 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Nov 16 11:32:28 1998 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Nov 16 11:32:54 1998 +0100
@@ -208,7 +208,7 @@
   in Thm.instantiate (cenvT, cenv) thm end;
 
 
-val insts = Scan.lift (Args.enum1 "and" (Args.var --| Args.$$$ "=" -- Args.name));
+fun insts x = Scan.lift (Args.enum1 "and" (Args.var --| Args.$$$ "=" -- Args.name)) x;
 fun gen_where context_of = syntax (insts >> (Attribute.rule o read_instantiate context_of));
 
 val global_where = gen_where ProofContext.init;