Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/rule_insts.ML
changeset 27378 0968c0d0b969
parent 27282 432a5baa7546
child 27809 a1e409db516b 
--- a/src/Pure/Isar/rule_insts.ML	Sat Jun 28 15:17:24 2008 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Sat Jun 28 15:17:26 2008 +0200
@@ -406,7 +406,7 @@
 
 val insts =
   Scan.optional
-    (Args.enum1 "and" (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
+    (Args.and_list1 (Scan.lift (Args.name -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
       Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
 
 fun inst_args f src ctxt =
@@ -414,7 +414,7 @@
 
 val insts_var =
   Scan.optional
-    (Args.enum1 "and" (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
+    (Args.and_list1 (Scan.lift (Args.var -- (Args.$$$ "=" |-- Args.!!! Args.name))) --|
       Scan.lift (Args.$$$ "in")) [] -- Attrib.thms;
 
 fun inst_args_var f src ctxt =
isabelle