--- a/src/HOL/Tools/arith_data.ML Thu Jul 19 22:21:59 2012 +0200
+++ b/src/HOL/Tools/arith_data.ML Fri Jul 20 10:53:25 2012 +0200
@@ -112,7 +112,8 @@
fun simp_all_tac rules =
let val ss0 = HOL_ss addsimps rules
- in fn ss => ALLGOALS (simp_tac (Simplifier.inherit_context ss ss0)) end;
+ val safe_simp_tac = generic_simp_tac true (false, false, false)
+ in fn ss => ALLGOALS (safe_simp_tac (Simplifier.inherit_context ss ss0)) end;
fun simplify_meta_eq rules =
let val ss0 = HOL_basic_ss addsimps rules |> Simplifier.add_eqcong @{thm eq_cong2}