--- a/src/ZF/arith_data.ML Mon Nov 11 20:00:53 2013 +0100
+++ b/src/ZF/arith_data.ML Mon Nov 11 20:50:12 2013 +0100
@@ -221,7 +221,9 @@
end;
-Addsimprocs ArithData.nat_cancel;
+val _ =
+ Theory.setup (Simplifier.map_theory_simpset (fn ctxt =>
+ ctxt addsimprocs ArithData.nat_cancel));
(*examples: