src/ZF/arith_data.ML

--- a/src/ZF/arith_data.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/ZF/arith_data.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -204,19 +204,19 @@
      [@{term "l #+ m = n"}, @{term "l = m #+ n"},
       @{term "l #* m = n"}, @{term "l = m #* n"},
       @{term "succ(m) = n"}, @{term "m = succ(n)"}],
-    proc = K EqCancelNumerals.proc, identifier = []},
+    proc = K EqCancelNumerals.proc},
   Simplifier.make_simproc @{context} "natless_cancel_numerals"
    {lhss =
      [@{term "l #+ m < n"}, @{term "l < m #+ n"},
       @{term "l #* m < n"}, @{term "l < m #* n"},
       @{term "succ(m) < n"}, @{term "m < succ(n)"}],
-    proc = K LessCancelNumerals.proc, identifier = []},
+    proc = K LessCancelNumerals.proc},
   Simplifier.make_simproc @{context} "natdiff_cancel_numerals"
    {lhss =
      [@{term "(l #+ m) #- n"}, @{term "l #- (m #+ n)"},
       @{term "(l #* m) #- n"}, @{term "l #- (m #* n)"},
       @{term "succ(m) #- n"}, @{term "m #- succ(n)"}],
-    proc = K DiffCancelNumerals.proc, identifier = []}];
+    proc = K DiffCancelNumerals.proc}];
 
 end;