--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Sat Mar 22 18:19:57 2014 +0100
@@ -434,7 +434,7 @@
fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
val tvar_a_str = "'a"
-val tvar_a_z = ((tvar_a_str, 0), HOLogic.typeS)
+val tvar_a_z = ((tvar_a_str, 0), @{sort type})
val tvar_a = TVar tvar_a_z
val tvar_a_name = tvar_name tvar_a_z
val itself_name = `make_fixed_type_const @{type_name itself}
@@ -2404,7 +2404,7 @@
fun rationalize_decls thy (decls as decl :: (decls' as _ :: _)) =
let
- val T = result_type_of_decl decl |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
+ val T = result_type_of_decl decl |> map_type_tvar (fn (z, _) => TVar (z, @{sort type}))
in
if forall (type_generalization thy T o result_type_of_decl) decls' then [decl]
else decls
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML Sat Mar 22 18:19:57 2014 +0100
@@ -94,7 +94,7 @@
fun make_tfree ctxt w =
let val ww = "'" ^ w in
- TFree (ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))
+ TFree (ww, the_default @{sort type} (Variable.def_sort ctxt (ww, ~1)))
end
exception ATP_CLASS of string list
@@ -126,7 +126,7 @@
Sometimes variables from the ATP are indistinguishable from Isabelle variables, which
forces us to use a type parameter in all cases. *)
Type_Infer.param 0 ("'" ^ perhaps (unprefix_and_unascii tvar_prefix) a,
- (if null clss then HOLogic.typeS else map class_of_atp_class clss))))
+ (if null clss then @{sort type} else map class_of_atp_class clss))))
end
fun atp_type_of_atp_term (ATerm ((s, _), us)) = AType ((s, []), map atp_type_of_atp_term us)
@@ -175,7 +175,7 @@
else
(s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
-fun slack_fastype_of t = fastype_of t handle TERM _ => HOLogic.typeT
+fun slack_fastype_of t = fastype_of t handle TERM _ => Type_Infer.anyT @{sort type}
(* Cope with "tt(X) = X" atoms, where "X" is existentially quantified. *)
fun loose_aconv (Free (s, _), Free (s', _)) = s = s'
@@ -184,8 +184,8 @@
val spass_skolem_prefix = "sk" (* "skc" or "skf" *)
val vampire_skolem_prefix = "sK"
-(* First-order translation. No types are known for variables. "HOLogic.typeT" should allow them to
- be inferred. *)
+(* First-order translation. No types are known for variables. "Type_Infer.anyT @{sort type}"
+ should allow them to be inferred. *)
fun term_of_atp ctxt textual sym_tab =
let
val thy = Proof_Context.theory_of ctxt
@@ -206,7 +206,7 @@
if textual andalso length ts = 2 andalso loose_aconv (hd ts, List.last ts) then
@{const True}
else
- list_comb (Const (@{const_name HOL.eq}, HOLogic.typeT), ts)
+ list_comb (Const (@{const_name HOL.eq}, Type_Infer.anyT @{sort type}), ts)
end
else
(case unprefix_and_unascii const_prefix s of
@@ -248,7 +248,8 @@
NONE)
|> (fn SOME T => T
| NONE =>
- map slack_fastype_of term_ts ---> the_default HOLogic.typeT opt_T)
+ map slack_fastype_of term_ts --->
+ the_default (Type_Infer.anyT @{sort type}) opt_T)
val t =
if new_skolem then Var ((new_skolem_var_name_of_const s'', var_index), T)
else Const (unproxify_const s', T)
@@ -274,7 +275,7 @@
SOME T => map slack_fastype_of term_ts ---> T
| NONE =>
map slack_fastype_of ts --->
- (case tys of [ty] => typ_of_atp_type ctxt ty | _ => HOLogic.typeT))
+ (case tys of [ty] => typ_of_atp_type ctxt ty | _ => Type_Infer.anyT @{sort type}))
val t =
(case unprefix_and_unascii fixed_var_prefix s of
SOME s => Free (s, T)
--- a/src/HOL/Tools/BNF/bnf_comp.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML Sat Mar 22 18:19:57 2014 +0100
@@ -138,15 +138,15 @@
forall inner from inners. idead = dead *)
val (oDs, lthy1) = apfst (map TFree)
- (Variable.invent_types (replicate odead HOLogic.typeS) lthy);
+ (Variable.invent_types (replicate odead @{sort type}) lthy);
val (Dss, lthy2) = apfst (map (map TFree))
- (fold_map Variable.invent_types (map (fn n => replicate n HOLogic.typeS) ideads) lthy1);
+ (fold_map Variable.invent_types (map (fn n => replicate n @{sort type}) ideads) lthy1);
val (Ass, lthy3) = apfst (replicate ilive o map TFree)
- (Variable.invent_types (replicate ilive HOLogic.typeS) lthy2);
+ (Variable.invent_types (replicate ilive @{sort type}) lthy2);
val As = if ilive > 0 then hd Ass else [];
val Ass_repl = replicate olive As;
val (Bs, names_lthy) = apfst (map TFree)
- (Variable.invent_types (replicate ilive HOLogic.typeS) lthy3);
+ (Variable.invent_types (replicate ilive @{sort type}) lthy3);
val Bss_repl = replicate olive Bs;
val ((((fs', Qs'), Asets), xs), _) = names_lthy
@@ -363,11 +363,11 @@
(* TODO: check 0 < n <= live *)
val (Ds, lthy1) = apfst (map TFree)
- (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
+ (Variable.invent_types (replicate dead @{sort type}) lthy);
val ((killedAs, As), lthy2) = apfst (`(take n) o map TFree)
- (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
+ (Variable.invent_types (replicate live @{sort type}) lthy1);
val (Bs, _(*lthy3*)) = apfst (append killedAs o map TFree)
- (Variable.invent_types (replicate (live - n) HOLogic.typeS) lthy2);
+ (Variable.invent_types (replicate (live - n) @{sort type}) lthy2);
val ((Asets, lives), _(*names_lthy*)) = lthy
|> mk_Frees "A" (map HOLogic.mk_setT (drop n As))
@@ -462,11 +462,11 @@
(* TODO: check 0 < n *)
val (Ds, lthy1) = apfst (map TFree)
- (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
+ (Variable.invent_types (replicate dead @{sort type}) lthy);
val ((newAs, As), lthy2) = apfst (chop n o map TFree)
- (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy1);
+ (Variable.invent_types (replicate (n + live) @{sort type}) lthy1);
val ((newBs, Bs), _(*lthy3*)) = apfst (chop n o map TFree)
- (Variable.invent_types (replicate (n + live) HOLogic.typeS) lthy2);
+ (Variable.invent_types (replicate (n + live) @{sort type}) lthy2);
val (Asets, _(*names_lthy*)) = lthy
|> mk_Frees "A" (map HOLogic.mk_setT (newAs @ As));
@@ -553,11 +553,11 @@
fun unpermute xs = permute_like_unique (op =) dest src xs;
val (Ds, lthy1) = apfst (map TFree)
- (Variable.invent_types (replicate dead HOLogic.typeS) lthy);
+ (Variable.invent_types (replicate dead @{sort type}) lthy);
val (As, lthy2) = apfst (map TFree)
- (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
+ (Variable.invent_types (replicate live @{sort type}) lthy1);
val (Bs, _(*lthy3*)) = apfst (map TFree)
- (Variable.invent_types (replicate live HOLogic.typeS) lthy2);
+ (Variable.invent_types (replicate live @{sort type}) lthy2);
val (Asets, _(*names_lthy*)) = lthy
|> mk_Frees "A" (map HOLogic.mk_setT (permute As));
@@ -757,9 +757,9 @@
val nwits = nwits_of_bnf bnf;
val (As, lthy1) = apfst (map TFree)
- (Variable.invent_types (replicate live HOLogic.typeS) (fold Variable.declare_typ Ds lthy));
+ (Variable.invent_types (replicate live @{sort type}) (fold Variable.declare_typ Ds lthy));
val (Bs, _) = apfst (map TFree)
- (Variable.invent_types (replicate live HOLogic.typeS) lthy1);
+ (Variable.invent_types (replicate live @{sort type}) lthy1);
val (((fs, fs'), (Rs, Rs')), _(*names_lthy*)) = lthy
|> mk_Frees' "f" (map2 (curry op -->) As Bs)
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Sat Mar 22 18:19:57 2014 +0100
@@ -901,7 +901,7 @@
end;
val Ass0 = map (map prepare_type_arg o type_args_named_constrained_of_spec) specs;
- val unsorted_Ass0 = map (map (resort_tfree HOLogic.typeS)) Ass0;
+ val unsorted_Ass0 = map (map (resort_tfree @{sort type})) Ass0;
val unsorted_As = Library.foldr1 (merge_type_args fp) unsorted_Ass0;
val num_As = length unsorted_As;
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Sat Mar 22 18:19:57 2014 +0100
@@ -963,7 +963,7 @@
val (bs, mxs) = map_split (apfst fst) fixes;
val (arg_Ts, res_Ts) = map (strip_type o snd o fst #>> mk_tupleT_balanced) fixes |> split_list;
- val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ arg_Ts) of
+ val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ arg_Ts) of
[] => ()
| (b, _) :: _ => primcorec_error ("type of " ^ Binding.print b ^ " contains top sort"));
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Sat Mar 22 18:19:57 2014 +0100
@@ -447,7 +447,7 @@
| is_only_old_datatype _ = false;
val _ = if exists is_only_old_datatype arg_Ts then raise OLD_PRIMREC () else ();
- val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, HOLogic.typeS)) (bs ~~ res_Ts) of
+ val _ = (case filter_out (fn (_, T) => Sign.of_sort thy (T, @{sort type})) (bs ~~ res_Ts) of
[] => ()
| (b, _) :: _ => raise PRIMREC ("type of " ^ Binding.print b ^ " contains top sort", []));
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar_util.ML Sat Mar 22 18:19:57 2014 +0100
@@ -148,7 +148,7 @@
val mk_TFrees' = apfst (map TFree) oo Variable.invent_types;
-fun mk_TFrees n = mk_TFrees' (replicate n HOLogic.typeS);
+fun mk_TFrees n = mk_TFrees' (replicate n @{sort type});
fun mk_Frees' x Ts ctxt = mk_fresh_names ctxt (length Ts) x |>> (fn xs => `(map Free) (xs ~~ Ts));
fun mk_Freess' x Tss = fold_map2 mk_Frees' (mk_names (length Tss) x) Tss #>> split_list;
@@ -169,7 +169,7 @@
fun variant_tfrees ss =
apfst (map TFree) o
- variant_types (map (ensure_prefix "'") ss) (replicate (length ss) HOLogic.typeS);
+ variant_types (map (ensure_prefix "'") ss) (replicate (length ss) @{sort type});
(*Replace each Ti by Ui (starting from the leaves); inst = [(T1, U1), ..., (Tn, Un)].*)
fun typ_subst_nonatomic [] = I
--- a/src/HOL/Tools/Datatype/datatype.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype.ML Sat Mar 22 18:19:57 2014 +0100
@@ -373,7 +373,7 @@
fun mk_thm i =
let
- val Ts = map (TFree o rpair HOLogic.typeS) (Name.variant_list used (replicate i "'t"));
+ val Ts = map (TFree o rpair @{sort type}) (Name.variant_list used (replicate i "'t"));
val f = Free ("f", Ts ---> U);
in
Goal.prove_sorry_global thy [] []
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Sat Mar 22 18:19:57 2014 +0100
@@ -182,7 +182,7 @@
val rec_result_Ts =
map TFree
(Name.variant_list used (replicate (length descr') "'t") ~~
- replicate (length descr') HOLogic.typeS);
+ replicate (length descr') @{sort type});
val reccomb_fn_Ts = maps (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
@@ -251,7 +251,7 @@
val recTs = Datatype_Aux.get_rec_types descr';
val used = fold Term.add_tfree_namesT recTs [];
val newTs = take (length (hd descr)) recTs;
- val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
+ val T' = TFree (singleton (Name.variant_list used) "'t", @{sort type});
val case_fn_Ts = map (fn (i, (_, _, constrs)) =>
map (fn (_, cargs) =>
@@ -296,7 +296,7 @@
val recTs = Datatype_Aux.get_rec_types descr';
val used' = fold Term.add_tfree_namesT recTs [];
val newTs = take (length (hd descr)) recTs;
- val T' = TFree (singleton (Name.variant_list used') "'t", HOLogic.typeS);
+ val T' = TFree (singleton (Name.variant_list used') "'t", @{sort type});
val P = Free ("P", T' --> HOLogic.boolT);
fun make_split (((_, (_, _, constrs)), T), comb_t) =
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Sat Mar 22 18:19:57 2014 +0100
@@ -36,7 +36,7 @@
else map (fn i => "P" ^ string_of_int i) (1 upto length descr);
val rec_result_Ts = map (fn ((i, _), P) =>
- if member (op =) is i then TFree ("'" ^ P, HOLogic.typeS) else HOLogic.unitT)
+ if member (op =) is i then TFree ("'" ^ P, @{sort type}) else HOLogic.unitT)
(descr ~~ pnames);
fun make_pred i T U r x =
@@ -163,8 +163,8 @@
let
val ctxt = Proof_Context.init_global thy;
val cert = cterm_of thy;
- val rT = TFree ("'P", HOLogic.typeS);
- val rT' = TVar (("'P", 0), HOLogic.typeS);
+ val rT = TFree ("'P", @{sort type});
+ val rT' = TVar (("'P", 0), @{sort type});
fun make_casedist_prem T (cname, cargs) =
let
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Sat Mar 22 18:19:57 2014 +0100
@@ -278,7 +278,7 @@
val recTs = Datatype_Aux.get_rec_types descr';
val used = fold Term.add_tfree_namesT recTs [];
val newTs = take (length (hd descr)) recTs;
- val T' = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS);
+ val T' = TFree (singleton (Name.variant_list used) "'t", @{sort type});
fun mk_dummyT dt = binder_types (Datatype_Aux.typ_of_dtyp descr' dt) ---> T';
--- a/src/HOL/Tools/Function/fun.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Function/fun.ML Sat Mar 22 18:19:57 2014 +0100
@@ -73,7 +73,7 @@
val qs = map Free (Name.invent Name.context "a" n ~~ argTs)
in
HOLogic.mk_eq(list_comb (Free (fname, fT), qs),
- Const ("HOL.undefined", rT))
+ Const (@{const_name undefined}, rT))
|> HOLogic.mk_Trueprop
|> fold_rev Logic.all qs
end
--- a/src/HOL/Tools/Function/function.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Function/function.ML Sat Mar 22 18:19:57 2014 +0100
@@ -156,7 +156,7 @@
end
val add_function =
- gen_add_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
+ gen_add_function false Specification.check_spec (Type_Infer.anyT @{sort type})
fun add_function_cmd a b c d int = gen_add_function int Specification.read_spec "_::type" a b c d
fun gen_function do_print prep default_constraint fixspec eqns config lthy =
@@ -170,7 +170,7 @@
end
val function =
- gen_function false Specification.check_spec (Type_Infer.anyT HOLogic.typeS)
+ gen_function false Specification.check_spec (Type_Infer.anyT @{sort type})
fun function_cmd a b c int = gen_function int Specification.read_spec "_::type" a b c
fun prepare_termination_proof prep_term raw_term_opt lthy =
--- a/src/HOL/Tools/Function/function_common.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Function/function_common.ML Sat Mar 22 18:19:57 2014 +0100
@@ -347,7 +347,7 @@
plural " " "s " not_defined ^ commas_quote not_defined)
fun check_sorts ((fname, fT), _) =
- Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, HOLogic.typeS)
+ Sorts.of_sort (Sign.classes_of (Proof_Context.theory_of ctxt)) (fT, @{sort type})
orelse error (cat_lines
["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Mar 22 18:19:57 2014 +0100
@@ -1053,7 +1053,7 @@
(Object_Logic.atomize_term thy prop)
val prop = HOLogic.mk_Trueprop (HOLogic.mk_imp (assm, concl))
|> map_types (map_type_tfree
- (fn (s, []) => TFree (s, HOLogic.typeS)
+ (fn (s, []) => TFree (s, @{sort type})
| x => TFree x))
val _ =
if debug then
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Sat Mar 22 18:19:57 2014 +0100
@@ -920,7 +920,7 @@
val Type ("fun", [T, T']) = fastype_of comb;
val (Const (case_name, _), fs) = strip_comb comb
val used = Term.add_tfree_names comb []
- val U = TFree (singleton (Name.variant_list used) "'t", HOLogic.typeS)
+ val U = TFree (singleton (Name.variant_list used) "'t", @{sort type})
val x = Free ("x", T)
val f = Free ("f", T' --> U)
fun apply_f f' =
@@ -947,8 +947,8 @@
val f = (fst (strip_comb (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of th))))))
val Type ("fun", [uninst_T, uninst_T']) = fastype_of f
val ([_, tname', uname, yname], ctxt') = Variable.add_fixes ["'t", "'t'", "'u", "y"] ctxt
- val T' = TFree (tname', HOLogic.typeS)
- val U = TFree (uname, HOLogic.typeS)
+ val T' = TFree (tname', @{sort type})
+ val U = TFree (uname, @{sort type})
val y = Free (yname, U)
val f' = absdummy (U --> T') (Bound 0 $ y)
val th' = Thm.certify_instantiate
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Sat Mar 22 18:19:57 2014 +0100
@@ -577,7 +577,7 @@
val pat_var_prefix = "_"
(* try "Long_Name.base_name" for shorter names *)
-fun massage_long_name s = if s = hd HOLogic.typeS then "T" else s
+fun massage_long_name s = if s = @{class type} then "T" else s
val crude_str_of_sort =
space_implode ":" o map massage_long_name o subtract (op =) @{sort type}
--- a/src/HOL/Tools/TFL/usyntax.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/TFL/usyntax.ML Sat Mar 22 18:19:57 2014 +0100
@@ -104,7 +104,7 @@
*
*---------------------------------------------------------------------------*)
val mk_prim_vartype = TVar;
-fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.typeS);
+fun mk_vartype s = mk_prim_vartype ((s, 0), @{sort type});
(* But internally, it's useful *)
fun dest_vtype (TVar x) = x
--- a/src/HOL/Tools/choice_specification.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/choice_specification.ML Sat Mar 22 18:19:57 2014 +0100
@@ -131,7 +131,7 @@
fun proc_single prop =
let
val frees = Misc_Legacy.term_frees prop
- val _ = forall (fn v => Sign.of_sort thy (type_of v,HOLogic.typeS)) frees
+ val _ = forall (fn v => Sign.of_sort thy (type_of v,@{sort type})) frees
orelse error "Specificaton: Only free variables of sort 'type' allowed"
val prop_closed = close_form prop
in
--- a/src/HOL/Tools/hologic.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/hologic.ML Sat Mar 22 18:19:57 2014 +0100
@@ -6,8 +6,6 @@
signature HOLOGIC =
sig
- val typeS: sort
- val typeT: typ
val id_const: typ -> term
val mk_comp: term * term -> term
val boolN: string
@@ -141,12 +139,6 @@
structure HOLogic: HOLOGIC =
struct
-(* HOL syntax *)
-
-val typeS: sort = ["HOL.type"];
-val typeT = Type_Infer.anyT typeS;
-
-
(* functions *)
fun id_const T = Const ("Fun.id", T --> T);
--- a/src/HOL/Tools/inductive_realizer.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Sat Mar 22 18:19:57 2014 +0100
@@ -53,8 +53,8 @@
| _ => vs)) (Term.add_vars prop []) [];
val attach_typeS = map_types (map_atyps
- (fn TFree (s, []) => TFree (s, HOLogic.typeS)
- | TVar (ixn, []) => TVar (ixn, HOLogic.typeS)
+ (fn TFree (s, []) => TFree (s, @{sort type})
+ | TVar (ixn, []) => TVar (ixn, @{sort type})
| T => T));
fun dt_of_intrs thy vs nparms intrs =
--- a/src/HOL/Tools/record.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/record.ML Sat Mar 22 18:19:57 2014 +0100
@@ -1819,7 +1819,7 @@
val all_vars = parent_vars @ vars;
val all_named_vars = (parent_names ~~ parent_vars) @ named_vars;
- val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", HOLogic.typeS);
+ val zeta = (singleton (Name.variant_list (map #1 alphas)) "'z", @{sort type});
val moreT = TFree zeta;
val more = Free (moreN, moreT);
val full_moreN = full (Binding.name moreN);
--- a/src/HOL/Tools/transfer.ML Sat Mar 22 18:16:54 2014 +0100
+++ b/src/HOL/Tools/transfer.ML Sat Mar 22 18:19:57 2014 +0100
@@ -467,7 +467,7 @@
| go _ ctxt = dummy ctxt
in
go t ctxt |> fst |> Syntax.check_term ctxt |>
- map_types (map_type_tfree (fn (a, _) => TFree (a, HOLogic.typeS)))
+ map_types (map_type_tfree (fn (a, _) => TFree (a, @{sort type})))
end
(** Monotonicity analysis **)
@@ -544,7 +544,7 @@
val relT = @{typ "bool => bool => bool"}
val idx = Thm.maxidx_of thm + 1
val thy = Proof_Context.theory_of ctxt
- fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), HOLogic.typeS)), cbool)
+ fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
in
thm
@@ -569,7 +569,7 @@
val relT = @{typ "bool => bool => bool"}
val idx = Thm.maxidx_of thm + 1
val thy = Proof_Context.theory_of ctxt
- fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), HOLogic.typeS)), cbool)
+ fun tinst (a, _) = (ctyp_of thy (TVar ((a, idx), @{sort type})), cbool)
fun inst (a, t) = (cterm_of thy (Var (Name.clean_index (prep a, idx), relT)), cterm_of thy t)
in
thm