--- a/src/HOL/Tools/inductive_realizer.ML Sun Dec 31 21:40:14 2023 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Sun Dec 31 22:04:41 2023 +0100
@@ -96,7 +96,7 @@
fun mk_realizes_eqn n vs nparms intrs =
let
- val intr = map_types Type.strip_sorts (Thm.prop_of (hd intrs));
+ val intr = Term.strip_sorts (Thm.prop_of (hd intrs));
val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl intr);
val iTs = rev (Term.add_tvars intr []);
val Tvs = map TVar iTs;
--- a/src/Pure/Isar/class.ML Sun Dec 31 21:40:14 2023 +0100
+++ b/src/Pure/Isar/class.ML Sun Dec 31 22:04:41 2023 +0100
@@ -190,7 +190,7 @@
val Ss = Sorts.mg_domain algebra tyco [class];
in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
- fun prt_param (c, ty) = pretty_param ctxt (c, Type.strip_sorts_dummy ty);
+ fun prt_param (c, ty) = pretty_param ctxt (c, Same.commit (Term.smash_sortsT_same dummyS) ty);
fun prt_entry class =
Pretty.block
@@ -394,11 +394,10 @@
val b_def = Binding.suffix_name "_dict" b;
val c = Sign.full_name thy b;
val ty = map Term.fastype_of dangling_params ---> Term.fastype_of rhs;
- val def_eq = Logic.mk_equals (list_comb (Const (c, ty), dangling_params), rhs)
- |> map_types Type.strip_sorts;
+ val def_eq = Term.strip_sorts (Logic.mk_equals (list_comb (Const (c, ty), dangling_params), rhs));
in
thy
- |> Sign.declare_const_global ((b, Type.strip_sorts ty), mx)
+ |> Sign.declare_const_global ((b, Term.strip_sortsT ty), mx)
|> snd
|> global_def (b_def, def_eq)
|-> (fn def_thm => register_def class def_thm)
--- a/src/Pure/Isar/class_declaration.ML Sun Dec 31 21:40:14 2023 +0100
+++ b/src/Pure/Isar/class_declaration.ML Sun Dec 31 22:04:41 2023 +0100
@@ -280,7 +280,7 @@
val b = Binding.name raw_c;
val c = Sign.full_name thy b;
val ty = map_atyps (K (Term.aT base_sort)) raw_ty;
- val ty0 = Type.strip_sorts ty;
+ val ty0 = Term.strip_sortsT ty;
val ty' = map_atyps (K (Term.aT [class])) ty0;
val syn = (the_default NoSyn o AList.lookup Binding.eq_name global_syntax) b;
in
--- a/src/Pure/Isar/code.ML Sun Dec 31 21:40:14 2023 +0100
+++ b/src/Pure/Isar/code.ML Sun Dec 31 22:04:41 2023 +0100
@@ -107,7 +107,7 @@
(* constants *)
-fun const_typ thy = Type.strip_sorts o Sign.the_const_type thy;
+fun const_typ thy = Term.strip_sortsT o Sign.the_const_type thy;
fun args_number thy = length o binder_types o const_typ thy;
@@ -119,7 +119,7 @@
in Term.typ_subst_TVars mapping ty end;
fun typscheme thy (c, ty) =
- (map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
+ (map dest_TFree (Sign.const_typargs thy (c, ty)), Term.strip_sortsT ty);
fun typscheme_equiv (ty1, ty2) =
Type.raw_instance (devarify ty1, ty2) andalso Type.raw_instance (devarify ty2, ty1);
@@ -1383,7 +1383,7 @@
fun subsumptive_add thy verbose (thm, proper) eqns =
let
val args_of = drop_prefix is_Var o rev o snd o strip_comb
- o Term.map_types Type.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of
+ o Term.strip_sorts o fst o Logic.dest_equals o Thm.plain_prop_of
o Thm.transfer thy;
val args = args_of thm;
val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
--- a/src/Pure/Proof/extraction.ML Sun Dec 31 21:40:14 2023 +0100
+++ b/src/Pure/Proof/extraction.ML Sun Dec 31 22:04:41 2023 +0100
@@ -389,7 +389,7 @@
(build_rev (Term.add_vars prop'));
val cs = maps (fn T => map (pair T) S) Ts;
val constraints' = map Logic.mk_of_class cs;
- val typ_map = Type.strip_sorts o
+ val typ_map = Term.strip_sortsT o
Term.map_atyps (fn U =>
if member (op =) atyps U
then #typ_operation ucontext {strip_sorts = false} U
@@ -417,8 +417,8 @@
thy |> ExtractionData.put
(if is_def then
{realizes_eqns = realizes_eqns,
- typeof_eqns = add_rule ([], Logic.dest_equals (map_types
- Type.strip_sorts (Thm.prop_of (Drule.abs_def thm)))) typeof_eqns,
+ typeof_eqns = typeof_eqns
+ |> add_rule ([], Logic.dest_equals (Term.strip_sorts (Thm.prop_of (Drule.abs_def thm)))),
types = types,
realizers = realizers, defs = insert Thm.eq_thm_prop (Thm.trim_context thm) defs,
expand = expand, prep = prep}
--- a/src/Pure/Proof/proof_rewrite_rules.ML Sun Dec 31 21:40:14 2023 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Sun Dec 31 22:04:41 2023 +0100
@@ -264,8 +264,7 @@
fun elim_defs thy r defs prf =
let
- val defs' = map (Logic.dest_equals o
- map_types Type.strip_sorts o Thm.prop_of o Drule.abs_def) defs;
+ val defs' = map (Logic.dest_equals o Term.strip_sorts o Thm.prop_of o Drule.abs_def) defs;
val defnames = map Thm.derivation_name defs;
val prf' =
if r then
@@ -375,7 +374,7 @@
in
map2 reconstruct (Logic.mk_of_sort (T, S))
(Proofterm.of_sort_proof (Sign.classes_of thy) (Thm.sorts_proof thy)
- (PClass o apfst Type.strip_sorts) (subst T, S))
+ (PClass o apfst Term.strip_sortsT) (subst T, S))
end;
fun expand_of_class_proof thy hyps (T, c) =
--- a/src/Pure/Thy/export_theory.ML Sun Dec 31 21:40:14 2023 +0100
+++ b/src/Pure/Thy/export_theory.ML Sun Dec 31 22:04:41 2023 +0100
@@ -243,9 +243,8 @@
let
val syntax = get_syntax_const thy_ctxt c;
val U = Logic.unvarifyT_global T;
- val U0 = Type.strip_sorts U;
- val trim_abbrev =
- Proofterm.standard_vars_term Name.context #> map_types Type.strip_sorts;
+ val U0 = Term.strip_sortsT U;
+ val trim_abbrev = Proofterm.standard_vars_term Name.context #> Term.strip_sorts;
val abbrev' = Option.map trim_abbrev abbrev;
val args = map (#1 o dest_TFree) (Consts.typargs consts (c, U0));
val propositional = Object_Logic.is_propositional thy_ctxt (Term.body_type U0);
--- a/src/Pure/axclass.ML Sun Dec 31 21:40:14 2023 +0100
+++ b/src/Pure/axclass.ML Sun Dec 31 22:04:41 2023 +0100
@@ -227,7 +227,7 @@
val tyco = inst_tyco_of thy (c, T);
val name_inst = instance_name (tyco, class) ^ "_inst";
val c' = instance_name (tyco, c);
- val T' = Type.strip_sorts T;
+ val T' = Term.strip_sortsT T;
in
thy
|> Sign.qualified_path true (Binding.name name_inst)
--- a/src/Pure/logic.ML Sun Dec 31 21:40:14 2023 +0100
+++ b/src/Pure/logic.ML Sun Dec 31 22:04:41 2023 +0100
@@ -382,10 +382,10 @@
fun atyp_operation {strip_sorts} =
Same.function_eq (op =) (fn T =>
(case AList.lookup (op =) present_map T of
- SOME T' => T' |> strip_sorts ? Type.strip_sorts
+ SOME T' => T' |> strip_sorts ? Term.strip_sortsT
| NONE =>
(case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of
- SOME T' => T' |> strip_sorts ? Type.strip_sorts
+ SOME T' => T' |> strip_sorts ? Term.strip_sortsT
| NONE => raise TYPE ("Dangling type variable ", [T], [prop]))));
val typ_operation = Term.map_atyps_same o atyp_operation;
--- a/src/Pure/proofterm.ML Sun Dec 31 21:40:14 2023 +0100
+++ b/src/Pure/proofterm.ML Sun Dec 31 22:04:41 2023 +0100
@@ -1654,7 +1654,7 @@
(case Sign.const_type thy s of
NONE => error ("reconstruct_proof: No such constant: " ^ quote s)
| SOME T =>
- let val T' = Type.strip_sorts (Logic.incr_tvar (maxidx + 1) T) in
+ let val T' = Term.strip_sortsT (Logic.incr_tvar (maxidx + 1) T) in
(Const (s, T'), T', vTs,
Envir.Envir {maxidx = maxidx + 1, tenv = tenv, tyenv = tyenv})
end)
--- a/src/Pure/term.ML Sun Dec 31 21:40:14 2023 +0100
+++ b/src/Pure/term.ML Sun Dec 31 22:04:41 2023 +0100
@@ -150,6 +150,10 @@
val declare_term_names: term -> Name.context -> Name.context
val declare_term_frees: term -> Name.context -> Name.context
val variant_frees: term -> (string * 'a) list -> (string * 'a) list
+ val smash_sortsT_same: sort -> typ Same.operation
+ val strip_sortsT_same: typ Same.operation
+ val strip_sortsT: typ -> typ
+ val strip_sorts: term -> term
val rename_wrt_term: term -> (string * 'a) list -> (string * 'a) list
val eq_ix: indexname * indexname -> bool
val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
@@ -579,6 +583,18 @@
fun rename_wrt_term t frees = rev (variant_frees t frees); (*reversed result!*)
+(* sorts *)
+
+fun smash_sortsT_same S' =
+ map_atyps_same
+ (fn TFree (x, S) => if S = S' then raise Same.SAME else TFree (x, S')
+ | TVar (xi, S) => if S = S' then raise Same.SAME else TVar (xi, S'));
+
+val strip_sortsT_same = smash_sortsT_same [];
+val strip_sortsT = Same.commit strip_sortsT_same;
+val strip_sorts = map_types strip_sortsT_same;
+
+
(** Comparing terms **)
--- a/src/Pure/type.ML Sun Dec 31 21:40:14 2023 +0100
+++ b/src/Pure/type.ML Sun Dec 31 22:04:41 2023 +0100
@@ -60,8 +60,6 @@
(*special treatment of type vars*)
val sort_of_atyp: typ -> sort
- val strip_sorts: typ -> typ
- val strip_sorts_dummy: typ -> typ
val no_tvars: typ -> typ
val varify_global_names: TFrees.set -> term -> ((string * sort) * (indexname * sort)) list
val varify_global: TFrees.set -> term -> ((string * sort) * (indexname * sort)) list * term
@@ -336,17 +334,6 @@
| sort_of_atyp T = raise TYPE ("sort_of_atyp", [T], []);
-(* strip_sorts *)
-
-val strip_sorts = map_atyps
- (fn TFree (x, _) => TFree (x, [])
- | TVar (xi, _) => TVar (xi, []));
-
-val strip_sorts_dummy = map_atyps
- (fn TFree (x, _) => TFree (x, dummyS)
- | TVar (xi, _) => TVar (xi, dummyS));
-
-
(* no_tvars *)
fun no_tvars T =
@@ -709,7 +696,7 @@
let
fun err msg =
cat_error msg ("The error(s) above occurred in type abbreviation " ^ Binding.print a);
- val rhs' = strip_sorts (no_tvars (cert_typ_mode mode_syntax tsig rhs))
+ val rhs' = Term.strip_sortsT (no_tvars (cert_typ_mode mode_syntax tsig rhs))
handle TYPE (msg, _, _) => err msg;
val _ =
(case duplicates (op =) vs of
--- a/src/Pure/type_infer_context.ML Sun Dec 31 21:40:14 2023 +0100
+++ b/src/Pure/type_infer_context.ML Sun Dec 31 22:04:41 2023 +0100
@@ -23,7 +23,7 @@
val const_sorts = Config.declare_bool ("const_sorts", \<^here>) (K true);
fun const_type ctxt =
- try ((not (Config.get ctxt const_sorts) ? Type.strip_sorts) o
+ try ((not (Config.get ctxt const_sorts) ? Term.strip_sortsT) o
Consts.the_constraint (Proof_Context.consts_of ctxt));
fun var_type ctxt = the_default dummyT o Proof_Context.def_type ctxt;
--- a/src/Tools/Code/code_thingol.ML Sun Dec 31 21:40:14 2023 +0100
+++ b/src/Tools/Code/code_thingol.ML Sun Dec 31 22:04:41 2023 +0100
@@ -532,7 +532,7 @@
let
val erase = map_types (fn _ => Type_Infer.anyT []);
val reinfer = singleton (Type_Infer_Context.infer_types ctxt);
- val lhs = list_comb (Const (c, ty), map (map_types Type.strip_sorts o snd) args);
+ val lhs = list_comb (Const (c, ty), map (Term.strip_sorts o snd) args);
val reinferred_rhs = snd (Logic.dest_equals (reinfer (Logic.mk_equals (lhs, erase rhs))));
in tag_term algbr eqngr reinferred_rhs rhs end