src/HOL/Library/rewrite.ML

--- a/src/HOL/Library/rewrite.ML	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Library/rewrite.ML	Sun Oct 18 21:30:01 2015 +0200
@@ -343,7 +343,7 @@
           | append_default (For x :: (ps as In :: Term _:: _)) = For x :: Concl :: ps
           | append_default ps = ps
 
-      in Scan.repeat sep_atom >> (flat #> rev #> append_default) end
+      in Scan.repeats sep_atom >> (rev #> append_default) end
 
     fun context_lift (scan : 'a parser) f = fn (context : Context.generic, toks) =>
       let