src/HOL/Tools/SMT/smt_real.ML
changeset 51717 9e7d1c139569
parent 47965 8ba6438557bc
     1.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -121,7 +121,7 @@
     1.4    by auto}
     1.5  
     1.6  val real_linarith_proc = Simplifier.simproc_global @{theory} "fast_real_arith" [
     1.7 -  "(m::real) < n", "(m::real) <= n", "(m::real) = n"] (K Lin_Arith.simproc)
     1.8 +  "(m::real) < n", "(m::real) <= n", "(m::real) = n"] Lin_Arith.simproc
     1.9  
    1.10  
    1.11  (* setup *)