--- 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,