Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/refute.ML
changeset 56243 2e10a36b8d46
parent 56147 9589605bcf41
child 56245 84fc7dfa3cd4 
--- a/src/HOL/Library/refute.ML	Fri Mar 21 12:14:33 2014 +0100
+++ b/src/HOL/Library/refute.ML	Fri Mar 21 12:34:50 2014 +0100
@@ -548,7 +548,7 @@
         Const (@{const_name all}, _) => t
       | Const (@{const_name "=="}, _) => t
       | Const (@{const_name "==>"}, _) => t
-      | Const (@{const_name TYPE}, _) => t  (* axiomatic type classes *)
+      | Const (@{const_name Pure.type}, _) => t  (* axiomatic type classes *)
       (* HOL *)
       | Const (@{const_name Trueprop}, _) => t
       | Const (@{const_name Not}, _) => t
@@ -713,7 +713,7 @@
       | Const (@{const_name "=="}, _) => axs
       | Const (@{const_name "==>"}, _) => axs
       (* axiomatic type classes *)
-      | Const (@{const_name TYPE}, T) => collect_type_axioms T axs
+      | Const (@{const_name Pure.type}, T) => collect_type_axioms T axs
       (* HOL *)
       | Const (@{const_name Trueprop}, _) => axs
       | Const (@{const_name Not}, _) => axs
isabelle