src/HOL/Library/Old_SMT/old_smt_real.ML

--- a/src/HOL/Library/Old_SMT/old_smt_real.ML	Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Library/Old_SMT/old_smt_real.ML	Fri Apr 08 20:15:20 2016 +0200
@@ -117,7 +117,7 @@
 val real_linarith_proc =
   Simplifier.make_simproc @{context} "fast_real_arith"
    {lhss = [@{term "(m::real) < n"}, @{term "(m::real) \<le> n"}, @{term "(m::real) = n"}],
-    proc = K Lin_Arith.simproc, identifier = []}
+    proc = K Lin_Arith.simproc}
 
 
 (* setup *)