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.
and_list;
authorwenzelm
Fri, 16 Apr 1999 17:48:46 +0200
changeset 6448 932f27366c8f
parent 6447 83d8dabdae9a
child 6449 d031cb5ea2fc
and_list;
src/Pure/Isar/attrib.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/attrib.ML	Fri Apr 16 17:48:31 1999 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Apr 16 17:48:46 1999 +0200
@@ -203,7 +203,7 @@
         (gen_distinct (fn ((x1, t1), (x2, t2)) => x1 = x2 andalso t1 aconv t2) (xs ~~ ts));
   in Thm.instantiate (cenvT, cenv) thm end;
 
-fun insts x = Scan.lift (Args.enum "and" (Args.var --| Args.$$$ "=" -- Args.name)) x;
+fun insts x = Args.and_list (Scan.lift (Args.var --| Args.$$$ "=" -- Args.name)) x;
 
 fun gen_where context_of = syntax (insts >> (Drule.rule_attribute o read_instantiate context_of));
isabelle