src/HOL/Tools/refute.ML
changeset 37677 c5a8b612e571
parent 37603 6e89e103f7c7
child 38553 56965d8e4e11
     1.1 --- a/src/HOL/Tools/refute.ML	Thu Jul 01 16:54:42 2010 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Thu Jul 01 16:54:42 2010 +0200
     1.3 @@ -653,7 +653,7 @@
     1.4        | Const (@{const_name "op -->"}, _) => t
     1.5        (* sets *)
     1.6        | Const (@{const_name Collect}, _) => t
     1.7 -      | Const (@{const_name "op :"}, _) => t
     1.8 +      | Const (@{const_name Set.member}, _) => t
     1.9        (* other optimizations *)
    1.10        | Const (@{const_name Finite_Set.card}, _) => t
    1.11        | Const (@{const_name Finite_Set.finite}, _) => t
    1.12 @@ -829,7 +829,7 @@
    1.13        | Const (@{const_name "op -->"}, _) => axs
    1.14        (* sets *)
    1.15        | Const (@{const_name Collect}, T) => collect_type_axioms T axs
    1.16 -      | Const (@{const_name "op :"}, T) => collect_type_axioms T axs
    1.17 +      | Const (@{const_name Set.member}, T) => collect_type_axioms T axs
    1.18        (* other optimizations *)
    1.19        | Const (@{const_name Finite_Set.card}, T) => collect_type_axioms T axs
    1.20        | Const (@{const_name Finite_Set.finite}, T) =>
    1.21 @@ -2634,11 +2634,11 @@
    1.22        | Const (@{const_name Collect}, _) =>
    1.23          SOME (interpret thy model args (eta_expand t 1))
    1.24        (* 'op :' == application *)
    1.25 -      | Const (@{const_name "op :"}, _) $ t1 $ t2 =>
    1.26 +      | Const (@{const_name Set.member}, _) $ t1 $ t2 =>
    1.27          SOME (interpret thy model args (t2 $ t1))
    1.28 -      | Const (@{const_name "op :"}, _) $ t1 =>
    1.29 +      | Const (@{const_name Set.member}, _) $ t1 =>
    1.30          SOME (interpret thy model args (eta_expand t 1))
    1.31 -      | Const (@{const_name "op :"}, _) =>
    1.32 +      | Const (@{const_name Set.member}, _) =>
    1.33          SOME (interpret thy model args (eta_expand t 2))
    1.34        | _ => NONE)
    1.35    end;
    1.36 @@ -3050,7 +3050,7 @@
    1.37  
    1.38    fun Product_Type_fst_interpreter thy model args t =
    1.39      case t of
    1.40 -      Const (@{const_name fst}, Type ("fun", [Type (@{type_name "*"}, [T, U]), _])) =>
    1.41 +      Const (@{const_name fst}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) =>
    1.42        let
    1.43          val constants_T = make_constants thy model T
    1.44          val size_U      = size_of_type thy model U
    1.45 @@ -3069,7 +3069,7 @@
    1.46  
    1.47    fun Product_Type_snd_interpreter thy model args t =
    1.48      case t of
    1.49 -      Const (@{const_name snd}, Type ("fun", [Type (@{type_name "*"}, [T, U]), _])) =>
    1.50 +      Const (@{const_name snd}, Type ("fun", [Type (@{type_name Product_Type.prod}, [T, U]), _])) =>
    1.51        let
    1.52          val size_T      = size_of_type thy model T
    1.53          val constants_U = make_constants thy model U