src/HOL/Decision_Procs/approximation.ML

--- a/src/HOL/Decision_Procs/approximation.ML	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/Decision_Procs/approximation.ML	Thu Feb 15 12:11:00 2018 +0100
@@ -105,9 +105,9 @@
 
 fun calculated_subterms (@{const Trueprop} $ t) = calculated_subterms t
   | calculated_subterms (@{const HOL.implies} $ _ $ t) = calculated_subterms t
-  | calculated_subterms (@{term "(<=) :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
+  | calculated_subterms (@{term "(\<le>) :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
   | calculated_subterms (@{term "(<) :: real \<Rightarrow> real \<Rightarrow> bool"} $ t1 $ t2) = [t1, t2]
-  | calculated_subterms (@{term "(:) :: real \<Rightarrow> real set \<Rightarrow> bool"} $ t1 $
+  | calculated_subterms (@{term "(\<in>) :: real \<Rightarrow> real set \<Rightarrow> bool"} $ t1 $
                          (@{term "atLeastAtMost :: real \<Rightarrow> real \<Rightarrow> real set"} $ t2 $ t3)) = [t1, t2, t3]
   | calculated_subterms t = raise TERM ("calculated_subterms", [t])
 
@@ -246,7 +246,7 @@
          |> approximate ctxt
          |> HOLogic.dest_list
          |> curry ListPair.zip (HOLogic.dest_list xs @ calculated_subterms arith_term)
-         |> map (fn (elem, s) => @{term "(:) :: real \<Rightarrow> real set \<Rightarrow> bool"} $ elem $ mk_result prec (dest_ivl s))
+         |> map (fn (elem, s) => @{term "(\<in>) :: real \<Rightarrow> real set \<Rightarrow> bool"} $ elem $ mk_result prec (dest_ivl s))
          |> foldr1 HOLogic.mk_conj))
 
 fun approx_arith prec ctxt t = realify t