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