src/HOL/Groebner_Basis.thy
changeset 61476 1884c40f1539
parent 60758 d8d85a8172b5
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Groebner_Basis.thy	Sun Oct 18 20:48:24 2015 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Sun Oct 18 21:30:01 2015 +0200
     1.3 @@ -41,7 +41,7 @@
     1.4      val addN = "add"
     1.5      val delN = "del"
     1.6      val any_keyword = keyword addN || keyword delN
     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 (keyword addN |-- thms) [] --
    1.11       Scan.optional (keyword delN |-- thms) [] >>