src/Pure/Isar/attrib.ML

     val cenvT = map (apsnd (Thm.ctyp_of sign)) envT;
     val cenv = map2 (fn (xi, t) => pairself (Thm.cterm_of sign) (Var (xi, fastype_of t), t)) (xs, ts);
   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;
 val local_where = gen_where I;