--- a/src/ZF/int_arith.ML Thu Jul 23 18:44:08 2009 +0200
+++ b/src/ZF/int_arith.ML Thu Jul 23 18:44:09 2009 +0200
@@ -145,7 +145,7 @@
val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
fun numeral_simp_tac ss =
ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
- THEN ALLGOALS (asm_simp_tac (local_simpset_of (Simplifier.the_context ss)))
+ THEN ALLGOALS (asm_simp_tac (simpset_of (Simplifier.the_context ss)))
val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s)
end;