src/HOL/Library/refute.ML
changeset 56252 b72e0a9d62b9
parent 56245 84fc7dfa3cd4
child 56256 1e01c159e7d9
     1.1 --- a/src/HOL/Library/refute.ML	Sat Mar 22 18:12:08 2014 +0100
     1.2 +++ b/src/HOL/Library/refute.ML	Sat Mar 22 18:15:09 2014 +0100
     1.3 @@ -579,7 +579,7 @@
     1.4            Type ("fun", [@{typ nat}, @{typ nat}])])) => t
     1.5        | Const (@{const_name Groups.times}, Type ("fun", [@{typ nat},
     1.6            Type ("fun", [@{typ nat}, @{typ nat}])])) => t
     1.7 -      | Const (@{const_name List.append}, _) => t
     1.8 +      | Const (@{const_name append}, _) => t
     1.9  (* UNSOUND
    1.10        | Const (@{const_name lfp}, _) => t
    1.11        | Const (@{const_name gfp}, _) => t
    1.12 @@ -684,11 +684,11 @@
    1.13      and collect_type_axioms T axs =
    1.14        case T of
    1.15        (* simple types *)
    1.16 -        Type ("prop", []) => axs
    1.17 -      | Type ("fun", [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs)
    1.18 +        Type (@{type_name prop}, []) => axs
    1.19 +      | Type (@{type_name fun}, [T1, T2]) => collect_type_axioms T2 (collect_type_axioms T1 axs)
    1.20        | Type (@{type_name set}, [T1]) => collect_type_axioms T1 axs
    1.21        (* axiomatic type classes *)
    1.22 -      | Type ("itself", [T1]) => collect_type_axioms T1 axs
    1.23 +      | Type (@{type_name itself}, [T1]) => collect_type_axioms T1 axs
    1.24        | Type (s, Ts) =>
    1.25          (case Datatype.get_info thy s of
    1.26            SOME _ =>  (* inductive datatype *)
    1.27 @@ -761,7 +761,7 @@
    1.28        | Const (@{const_name Groups.times}, T as Type ("fun", [@{typ nat},
    1.29          Type ("fun", [@{typ nat}, @{typ nat}])])) =>
    1.30            collect_type_axioms T axs
    1.31 -      | Const (@{const_name List.append}, T) => collect_type_axioms T axs
    1.32 +      | Const (@{const_name append}, T) => collect_type_axioms T axs
    1.33  (* UNSOUND
    1.34        | Const (@{const_name lfp}, T) => collect_type_axioms T axs
    1.35        | Const (@{const_name gfp}, T) => collect_type_axioms T axs
    1.36 @@ -819,8 +819,8 @@
    1.37      val thy = Proof_Context.theory_of ctxt
    1.38      fun collect_types T acc =
    1.39        (case T of
    1.40 -        Type ("fun", [T1, T2]) => collect_types T1 (collect_types T2 acc)
    1.41 -      | Type ("prop", []) => acc
    1.42 +        Type (@{type_name fun}, [T1, T2]) => collect_types T1 (collect_types T2 acc)
    1.43 +      | Type (@{type_name prop}, []) => acc
    1.44        | Type (@{type_name set}, [T1]) => collect_types T1 acc
    1.45        | Type (s, Ts) =>
    1.46            (case Datatype.get_info thy s of
    1.47 @@ -2620,11 +2620,12 @@
    1.48  
    1.49  fun List_append_interpreter ctxt model args t =
    1.50    case t of
    1.51 -    Const (@{const_name List.append}, Type ("fun", [Type ("List.list", [T]), Type ("fun",
    1.52 -        [Type ("List.list", [_]), Type ("List.list", [_])])])) =>
    1.53 +    Const (@{const_name append},
    1.54 +      Type (@{type_name fun}, [Type (@{type_name list}, [T]),
    1.55 +        Type (@{type_name fun}, [Type (@{type_name list}, [_]), Type (@{type_name list}, [_])])])) =>
    1.56        let
    1.57          val size_elem = size_of_type ctxt model T
    1.58 -        val size_list = size_of_type ctxt model (Type ("List.list", [T]))
    1.59 +        val size_list = size_of_type ctxt model (Type (@{type_name list}, [T]))
    1.60          (* maximal length of lists; 0 if we only consider the empty list *)
    1.61          val list_length =
    1.62            let
    1.63 @@ -2866,7 +2867,7 @@
    1.64          in
    1.65            SOME (fold_rev (fn pair => fn acc => HOLogic_insert $ pair $ acc) pairs HOLogic_empty_set)
    1.66          end
    1.67 -    | Type ("prop", []) =>
    1.68 +    | Type (@{type_name prop}, []) =>
    1.69          (case index_from_interpretation intr of
    1.70            ~1 => SOME (HOLogic.mk_Trueprop (Const (@{const_name undefined}, HOLogic.boolT)))
    1.71          | 0  => SOME (HOLogic.mk_Trueprop @{term True})