--- a/src/HOL/Library/bnf_decl.ML Sat Mar 22 18:12:08 2014 +0100
+++ b/src/HOL/Library/bnf_decl.ML Sat Mar 22 18:15:09 2014 +0100
@@ -94,7 +94,7 @@
val bnf_decl = prepare_decl (K I) (K I);
-fun read_constraint _ NONE = HOLogic.typeS
+fun read_constraint _ NONE = @{sort type}
| read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s;
val bnf_decl_cmd = prepare_decl read_constraint Syntax.read_typ;
--- 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})
--- a/src/HOL/Library/simps_case_conv.ML Sat Mar 22 18:12:08 2014 +0100
+++ b/src/HOL/Library/simps_case_conv.ML Sat Mar 22 18:15:09 2014 +0100
@@ -152,13 +152,12 @@
fun was_split t =
let
- val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq
- o fst o HOLogic.dest_imp
+ val is_free_eq_imp = is_Free o fst o HOLogic.dest_eq o fst o HOLogic.dest_imp
val get_conjs = HOLogic.dest_conj o HOLogic.dest_Trueprop
- fun dest_alls (Const ("HOL.All", _) $ Abs (_, _, t)) = dest_alls t
+ fun dest_alls (Const (@{const_name All}, _) $ Abs (_, _, t)) = dest_alls t
| dest_alls t = t
in forall (is_free_eq_imp o dest_alls) (get_conjs t) end
- handle TERM _ => false
+ handle TERM _ => false
fun apply_split ctxt split thm = Seq.of_list
let val ((_,thm'), ctxt') = Variable.import false [thm] ctxt in
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sat Mar 22 18:12:08 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sat Mar 22 18:15:09 2014 +0100
@@ -999,15 +999,15 @@
val is =
upto (1, arity)
|> map Int.toString
- val arg_tys = map (fn i => TFree ("arg" ^ i ^ "_ty", HOLogic.typeS)) is
- val res_ty = TFree ("res" ^ "_ty", HOLogic.typeS)
+ val arg_tys = map (fn i => TFree ("arg" ^ i ^ "_ty", @{sort type})) is
+ val res_ty = TFree ("res" ^ "_ty", @{sort type})
val f_ty = arg_tys ---> res_ty
val f = Free ("f", f_ty)
val xs = map (fn i =>
- Free ("x" ^ i, TFree ("arg" ^ i ^ "_ty", HOLogic.typeS))) is
+ Free ("x" ^ i, TFree ("arg" ^ i ^ "_ty", @{sort type}))) is
(*FIXME DRY principle*)
val ys = map (fn i =>
- Free ("y" ^ i, TFree ("arg" ^ i ^ "_ty", HOLogic.typeS))) is
+ Free ("y" ^ i, TFree ("arg" ^ i ^ "_ty", @{sort type}))) is
val hyp_lhs = list_comb (f, xs)
val hyp_rhs = list_comb (f, ys)
@@ -1018,7 +1018,7 @@
|> HOLogic.mk_Trueprop
fun conc_eq i =
let
- val ty = TFree ("arg" ^ i ^ "_ty", HOLogic.typeS)
+ val ty = TFree ("arg" ^ i ^ "_ty", @{sort type})
val x = Free ("x" ^ i, ty)
val y = Free ("y" ^ i, ty)
val eq = HOLogic.eq_const ty $ x $ y