src/HOL/Tools/refute.ML
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 39046 5b38730f3e12
     1.1 --- a/src/HOL/Tools/refute.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/refute.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -647,7 +647,7 @@
     1.4        | Const (@{const_name Hilbert_Choice.Eps}, _) => t
     1.5        | Const (@{const_name All}, _) => t
     1.6        | Const (@{const_name Ex}, _) => t
     1.7 -      | Const (@{const_name "op ="}, _) => t
     1.8 +      | Const (@{const_name HOL.eq}, _) => t
     1.9        | Const (@{const_name HOL.conj}, _) => t
    1.10        | Const (@{const_name HOL.disj}, _) => t
    1.11        | Const (@{const_name HOL.implies}, _) => t
    1.12 @@ -823,7 +823,7 @@
    1.13          end
    1.14        | Const (@{const_name All}, T) => collect_type_axioms T axs
    1.15        | Const (@{const_name Ex}, T) => collect_type_axioms T axs
    1.16 -      | Const (@{const_name "op ="}, T) => collect_type_axioms T axs
    1.17 +      | Const (@{const_name HOL.eq}, T) => collect_type_axioms T axs
    1.18        | Const (@{const_name HOL.conj}, _) => axs
    1.19        | Const (@{const_name HOL.disj}, _) => axs
    1.20        | Const (@{const_name HOL.implies}, _) => axs
    1.21 @@ -1850,16 +1850,16 @@
    1.22        end
    1.23      | Const (@{const_name Ex}, _) =>
    1.24        SOME (interpret thy model args (eta_expand t 1))
    1.25 -    | Const (@{const_name "op ="}, _) $ t1 $ t2 =>  (* similar to "==" (Pure) *)
    1.26 +    | Const (@{const_name HOL.eq}, _) $ t1 $ t2 =>  (* similar to "==" (Pure) *)
    1.27        let
    1.28          val (i1, m1, a1) = interpret thy model args t1
    1.29          val (i2, m2, a2) = interpret thy m1 a1 t2
    1.30        in
    1.31          SOME (make_equality (i1, i2), m2, a2)
    1.32        end
    1.33 -    | Const (@{const_name "op ="}, _) $ t1 =>
    1.34 +    | Const (@{const_name HOL.eq}, _) $ t1 =>
    1.35        SOME (interpret thy model args (eta_expand t 1))
    1.36 -    | Const (@{const_name "op ="}, _) =>
    1.37 +    | Const (@{const_name HOL.eq}, _) =>
    1.38        SOME (interpret thy model args (eta_expand t 2))
    1.39      | Const (@{const_name HOL.conj}, _) $ t1 $ t2 =>
    1.40        (* 3-valued logic *)