src/HOL/Library/refute.ML
changeset 56243 2e10a36b8d46
parent 56147 9589605bcf41
child 56245 84fc7dfa3cd4
     1.1 --- a/src/HOL/Library/refute.ML	Fri Mar 21 12:14:33 2014 +0100
     1.2 +++ b/src/HOL/Library/refute.ML	Fri Mar 21 12:34:50 2014 +0100
     1.3 @@ -548,7 +548,7 @@
     1.4          Const (@{const_name all}, _) => t
     1.5        | Const (@{const_name "=="}, _) => t
     1.6        | Const (@{const_name "==>"}, _) => t
     1.7 -      | Const (@{const_name TYPE}, _) => t  (* axiomatic type classes *)
     1.8 +      | Const (@{const_name Pure.type}, _) => t  (* axiomatic type classes *)
     1.9        (* HOL *)
    1.10        | Const (@{const_name Trueprop}, _) => t
    1.11        | Const (@{const_name Not}, _) => t
    1.12 @@ -713,7 +713,7 @@
    1.13        | Const (@{const_name "=="}, _) => axs
    1.14        | Const (@{const_name "==>"}, _) => axs
    1.15        (* axiomatic type classes *)
    1.16 -      | Const (@{const_name TYPE}, T) => collect_type_axioms T axs
    1.17 +      | Const (@{const_name Pure.type}, T) => collect_type_axioms T axs
    1.18        (* HOL *)
    1.19        | Const (@{const_name Trueprop}, _) => axs
    1.20        | Const (@{const_name Not}, _) => axs