--- 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})