# HG changeset patch
# User wenzelm
# Date 953309519 -3600
# Node ID 75fc67e56440dcf00cdba7a3e18590e73b75914b
# Parent  2ff3d25943f1239b0d48e3643d5d76790d293234
arith method: bang arg;

diff -r 2ff3d25943f1 -r 75fc67e56440 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Fri Mar 17 17:10:37 2000 +0100
+++ b/src/HOL/Arith.ML	Fri Mar 17 17:11:59 2000 +0100
@@ -1033,12 +1033,12 @@
 
 (* proof method setup *)
 
-val arith_method =
-  Method.METHOD (fn facts => FIRSTGOAL (Method.insert_tac facts THEN' arith_tac));
+fun arith_method prems =
+  Method.METHOD (fn facts => FIRSTGOAL (Method.insert_tac (prems @ facts) THEN' arith_tac));
 
 val arith_setup =
  [Method.add_methods
-  [("arith", Method.no_args arith_method, "decide linear arithmethic")]];
+  [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts , "decide linear arithmethic")]];
 
 (*---------------------------------------------------------------------------*)
 (* End of proof procedures. Now go and USE them!                             *)