src/HOL/Presburger.thy
changeset 61476 1884c40f1539
parent 60758 d8d85a8172b5
child 61799 4cf66f21b764
--- a/src/HOL/Presburger.thy	Sun Oct 18 20:48:24 2015 +0200
+++ b/src/HOL/Presburger.thy	Sun Oct 18 21:30:01 2015 +0200
@@ -400,7 +400,7 @@
     val delN = "del"
     val elimN = "elim"
     val any_keyword = keyword addN || keyword delN || simple_keyword elimN
-    val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat;
+    val thms = Scan.repeats (Scan.unless any_keyword Attrib.multi_thm)
   in
     Scan.optional (simple_keyword elimN >> K false) true --
     Scan.optional (keyword addN |-- thms) [] --