--- a/src/ZF/int_arith.ML Mon Nov 11 20:00:53 2013 +0100
+++ b/src/ZF/int_arith.ML Mon Nov 11 20:50:12 2013 +0100
@@ -320,10 +320,12 @@
end;
-
-Addsimprocs Int_Numeral_Simprocs.cancel_numerals;
-Addsimprocs [Int_Numeral_Simprocs.combine_numerals,
- Int_Numeral_Simprocs.combine_numerals_prod];
+val _ =
+ Theory.setup (Simplifier.map_theory_simpset (fn ctxt =>
+ ctxt addsimprocs
+ (Int_Numeral_Simprocs.cancel_numerals @
+ [Int_Numeral_Simprocs.combine_numerals,
+ Int_Numeral_Simprocs.combine_numerals_prod])));
(*examples:*)