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