src/ZF/arith_data.ML

       "succ(m) #- n", "m #- succ(n)"],
      DiffCancelNumerals.proc)];
 
 end;
 
-Addsimprocs ArithData.nat_cancel;
+val _ =
+  Theory.setup (Simplifier.map_theory_simpset (fn ctxt =>
+    ctxt addsimprocs ArithData.nat_cancel));
 
 
 (*examples:
 print_depth 22;
 set timing;