src/HOL/Library/refute.ML

--- a/src/HOL/Library/refute.ML	Sat Mar 22 18:12:08 2014 +0100
+++ b/src/HOL/Library/refute.ML	Sat Mar 22 18:15:09 2014 +0100
@@ -579,7 +579,7 @@
           Type ("fun", [@{typ nat}, @{typ nat}])])) => t
       | Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
           Type ("fun", [@{typ nat}, @{typ nat}])])) => t
-      | Const (@{const_name List.append}, _) => t
+      | Const (@{const_name append}, _) => t
 (* UNSOUND
       | Const (@{const_name lfp}, _) => t
       | Const (@{const_name gfp}, _) => t
@@ -684,11 +684,11 @@
     and collect_type_axioms T axs =
       case T of
       (* simple types *)
-        Type ("prop", []) => axs
-      | Type ("fun", [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs)
+        Type (@{type_name prop}, []) => axs
+      | Type (@{type_name fun}, [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs)
       | Type (@{type_name set}, [T1]) => collect_type_axioms T1 axs
       (* axiomatic type classes *)
-      | Type ("itself", [T1]) => collect_type_axioms T1 axs
+      | Type (@{type_name itself}, [T1]) => collect_type_axioms T1 axs
       | Type (s, Ts) =>
         (case Datatype.get_info thy s of
           SOME _ =>  (* inductive datatype *)
@@ -761,7 +761,7 @@
       | Const (@{const_name Groups.times}, T as Type ("fun", [@{typ nat},
         Type ("fun", [@{typ nat}, @{typ nat}])])) =>
           collect_type_axioms T axs
-      | Const (@{const_name List.append}, T) => collect_type_axioms T axs
+      | Const (@{const_name append}, T) => collect_type_axioms T axs
 (* UNSOUND
       | Const (@{const_name lfp}, T) => collect_type_axioms T axs
       | Const (@{const_name gfp}, T) => collect_type_axioms T axs
@@ -819,8 +819,8 @@
     val thy = Proof_Context.theory_of ctxt
     fun collect_types T acc =
       (case T of
-        Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc)
-      | Type ("prop", []) => acc
+        Type (@{type_name fun}, [T1, T2]) => collect_types T1 (collect_types T2 acc)
+      | Type (@{type_name prop}, []) => acc
       | Type (@{type_name set}, [T1]) => collect_types T1 acc
       | Type (s, Ts) =>
           (case Datatype.get_info thy s of
@@ -2620,11 +2620,12 @@
 
 fun List_append_interpreter ctxt model args t =
   case t of
-    Const (@{const_name List.append}, Type ("fun", [Type ("List.list", [T]), Type ("fun",
-        [Type ("List.list", [_]), Type ("List.list", [_])])])) =>
+    Const (@{const_name append},
+      Type (@{type_name fun}, [Type (@{type_name list}, [T]),
+        Type (@{type_name fun}, [Type (@{type_name list}, [_]), Type (@{type_name list}, [_])])])) =>
       let
         val size_elem = size_of_type ctxt model T
-        val size_list = size_of_type ctxt model (Type ("List.list", [T]))
+        val size_list = size_of_type ctxt model (Type (@{type_name list}, [T]))
         (* maximal length of lists; 0 if we only consider the empty list *)
         val list_length =
           let
@@ -2866,7 +2867,7 @@
         in
           SOME (fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) pairs HOLogic_empty_set)
         end
-    | Type ("prop", []) =>
+    | Type (@{type_name prop}, []) =>
         (case index_from_interpretation intr of
           ~1 => SOME (HOLogic.mk_Trueprop (Const (@{const_name undefined}, HOLogic.boolT)))
         | 0  => SOME (HOLogic.mk_Trueprop @{term True})