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/HOL/Library/rewrite.ML
changeset 63285 e9c777bfd78c
parent 62969 9f394a16c557
child 69593 3dda49e08b9d 
--- a/src/HOL/Library/rewrite.ML	Sat Jun 11 13:57:59 2016 +0200
+++ b/src/HOL/Library/rewrite.ML	Sat Jun 11 16:41:11 2016 +0200
@@ -333,7 +333,7 @@
         val sep = (Args.$$$ "at" >> K At) || (Args.$$$ "in" >> K In)
         val atom =  (Args.$$$ "asm" >> K Asm) ||
           (Args.$$$ "concl" >> K Concl) ||
-          (Args.$$$ "for" |-- Args.parens (Scan.optional Parse.fixes []) >> For) ||
+          (Args.$$$ "for" |-- Args.parens (Scan.optional Parse.vars []) >> For) ||
           (Parse.term >> Term)
         val sep_atom = sep -- atom >> (fn (s,a) => [s,a])
isabelle