# HG changeset patch
# User wenzelm
# Date 1330355151 -3600
# Node ID 65a9b30bff00da448bb8a10269ea5ca5ee51d1bb
# Parent  b138dee7bed321a9fe056919f2a8a5f74f23320f
clarified prems_lin_arith_tac, with subtle change of semantics: structured prems are inserted as well;

diff -r b138dee7bed3 -r 65a9b30bff00 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Mon Feb 27 15:48:02 2012 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Mon Feb 27 16:05:51 2012 +0100
@@ -901,7 +901,7 @@
 val setup =
   init_arith_data #>
   Simplifier.map_ss (fn ss => ss
-    addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.cut_lin_arith_tac)));
+    addSolver (mk_solver "lin_arith" (add_arith_facts #> Fast_Arith.prems_lin_arith_tac)));
 
 val global_setup =
   Attrib.setup @{binding arith_split} (Scan.succeed (Thm.declaration_attribute add_split))
diff -r b138dee7bed3 -r 65a9b30bff00 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Mon Feb 27 15:48:02 2012 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Mon Feb 27 16:05:51 2012 +0100
@@ -1,9 +1,7 @@
 (*  Title:      Provers/Arith/fast_lin_arith.ML
     Author:     Tobias Nipkow and Tjark Weber and Sascha Boehme
 
-A generic linear arithmetic package.  It provides two tactics
-(cut_lin_arith_tac, lin_arith_tac) and a simplification procedure
-(lin_arith_simproc).
+A generic linear arithmetic package.
 
 Only take premises and conclusions into account that are already
 (negated) (in)equations. lin_arith_simproc tries to prove or disprove
@@ -88,7 +86,7 @@
 
 signature FAST_LIN_ARITH =
 sig
-  val cut_lin_arith_tac: simpset -> int -> tactic
+  val prems_lin_arith_tac: simpset -> int -> tactic
   val lin_arith_tac: Proof.context -> bool -> int -> tactic
   val lin_arith_simproc: simpset -> term -> thm option
   val map_data:
@@ -846,8 +844,8 @@
                                refute_tac ss (i, split_neq, js))
   end);
 
-fun cut_lin_arith_tac ss =
-  cut_facts_tac (Simplifier.prems_of ss) THEN'
+fun prems_lin_arith_tac ss =
+  Method.insert_tac (Simplifier.prems_of ss) THEN'
   simpset_lin_arith_tac ss false;
 
 fun lin_arith_tac ctxt =