Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
made SML/NJ happy;
authorwenzelm
Mon, 16 Nov 1998 11:32:54 +0100
changeset 5894 71667e5c2ff8
parent 5893 c755dfd02509
child 5895 457b42674b57
made SML/NJ happy;
src/Pure/Isar/attrib.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle