src/ZF/arith_data.ML
changeset 54388 8b165615ffe3
parent 51717 9e7d1c139569
child 58838 59203adfc33f
--- 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: