# HG changeset patch
# User wenzelm
# Date 1127506911 -7200
# Node ID 61556de6ef4656ca43dee7ca4bf7b288f44b22d8
# Parent  58778df33e2f4d465ba38a952902c8477776d571
Provers/Arith/fast_lin_arith.ML: Simplifier.inherit_bounds;

diff -r 58778df33e2f -r 61556de6ef46 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Fri Sep 23 22:21:50 2005 +0200
+++ b/src/HOL/arith_data.ML	Fri Sep 23 22:21:51 2005 +0200
@@ -51,9 +51,9 @@
 
 val mk_eqv = HOLogic.mk_Trueprop o HOLogic.mk_eq;
 
-fun prove_conv expand_tac norm_tac sg tu =
+fun prove_conv expand_tac norm_tac sg ss tu =
   mk_meta_eq (prove_goalw_cterm_nocheck [] (cterm_of sg (mk_eqv tu))
-    (K [expand_tac, norm_tac]))
+    (K [expand_tac, norm_tac ss]))
   handle ERROR => error ("The error(s) above occurred while trying to prove " ^
     (string_of_cterm (cterm_of sg (mk_eqv tu))));
 
@@ -63,7 +63,8 @@
 
 (* rewriting *)
 
-fun simp_all rules = ALLGOALS (simp_tac (HOL_ss addsimps rules));
+fun simp_all_tac rules ss =
+  ALLGOALS (simp_tac (Simplifier.inherit_bounds ss HOL_ss addsimps rules));
 
 val add_rules = [add_Suc, add_Suc_right, add_0, add_0_right];
 val mult_rules = [mult_Suc, mult_Suc_right, mult_0, mult_0_right];
@@ -92,7 +93,7 @@
   val mk_sum = mk_norm_sum;
   val dest_sum = dest_sum;
   val prove_conv = prove_conv;
-  val norm_tac = simp_all add_rules THEN simp_all add_ac;
+  fun norm_tac ss = simp_all_tac add_rules ss THEN simp_all_tac add_ac ss;
 end;
 
 fun gen_uncancel_tac rule ct =
@@ -540,7 +541,7 @@
  [Simplifier.change_simpset_of (op addsimprocs) nat_cancel_sums] @
   init_lin_arith_data @
   [Simplifier.change_simpset_of (op addSolver)
-   (mk_solver "lin. arith." Fast_Arith.cut_lin_arith_tac),
+   (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac),
   Simplifier.change_simpset_of (op addsimprocs) [fast_nat_arith_simproc],
   Method.add_methods
       [("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,