diff -r 2eef5e71edd6 -r d2d7874648bd src/HOL/Presburger.thy --- a/src/HOL/Presburger.thy Mon Mar 16 17:51:24 2009 +0100 +++ b/src/HOL/Presburger.thy Mon Mar 16 18:24:30 2009 +0100 @@ -455,12 +455,11 @@ val any_keyword = keyword addN || keyword delN || simple_keyword elimN val thms = Scan.repeat (Scan.unless any_keyword Attrib.multi_thm) >> flat; in - fn src => Method.syntax - ((Scan.optional (simple_keyword elimN >> K false) true) -- - (Scan.optional (keyword addN |-- thms) []) -- - (Scan.optional (keyword delN |-- thms) [])) src - #> (fn (((elim, add_ths), del_ths),ctxt) => - SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt)) + Scan.optional (simple_keyword elimN >> K false) true -- + Scan.optional (keyword addN |-- thms) [] -- + Scan.optional (keyword delN |-- thms) [] >> + (fn ((elim, add_ths), del_ths) => fn ctxt => + SIMPLE_METHOD' (Presburger.cooper_tac elim add_ths del_ths ctxt)) end *} "Cooper's algorithm for Presburger arithmetic"