| changeset 5894 | 71667e5c2ff8 |
| parent 5879 | 18b8f048d93a |
| child 5912 | 3f95adea10c0 |
--- 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;