src/HOL/Tools/SMT/smt_real.ML
changeset 62913 13252110a6fe
parent 61144 5e94dfead1c2
child 66551 4df6b0ae900d
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Thu Apr 07 22:09:23 2016 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Fri Apr 08 20:15:20 2016 +0200
     1.3 @@ -101,7 +101,7 @@
     1.4  val real_linarith_proc =
     1.5    Simplifier.make_simproc @{context} "fast_real_arith"
     1.6     {lhss = [@{term "(m::real) < n"}, @{term "(m::real) \<le> n"}, @{term "(m::real) = n"}],
     1.7 -    proc = K Lin_Arith.simproc, identifier = []}
     1.8 +    proc = K Lin_Arith.simproc}
     1.9  
    1.10  
    1.11  (* setup *)