# HG changeset patch
# User wenzelm
# Date 1723056991 -7200
# Node ID cbfc1058df7c9a53edf9e51aa5bbe720beb95b7b
# Parent  10c712405854bb19cc2b00f0dbeb324ba155648f# Parent  e8a47adda46b8046ab6d2fbe4dce88d8d9f2f06f
merged

diff -r 10c712405854 -r cbfc1058df7c src/HOL/Data_Structures/Define_Time_Function.ML
--- a/src/HOL/Data_Structures/Define_Time_Function.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Data_Structures/Define_Time_Function.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -543,9 +543,9 @@
     (* Print result if print *)
     val _ = if not print then () else
         let
-          val nms = map (fst o dest_Const) term
+          val nms = map dest_Const_name term
           val used = map (used_for_const orig_used) term
-          val typs = map (snd o dest_Const) term
+          val typs = map dest_Const_type term
         in
           print_timing' print_ctxt { names=nms, terms=terms, typs=typs } { names=timing_names, terms=T_terms, typs=map (fn (used, typ) => change_typ' used 0 typ) (zip used typs) }
         end
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Finite_Set.thy	Wed Aug 07 20:56:31 2024 +0200
@@ -199,12 +199,12 @@
   val Eq_TrueI = @{thm Eq_TrueI}
 
   fun is_subset A th = case Thm.prop_of th of
-        (_ $ (Const (\<^const_name>\<open>less_eq\<close>, Type (\<^type_name>\<open>fun\<close>, [Type (\<^type_name>\<open>set\<close>, _), _])) $ A' $ B))
+        (_ $ \<^Const_>\<open>less_eq \<^Type>\<open>set _\<close> for A' B\<close>)
         => if A aconv A' then SOME(B,th) else NONE
       | _ => NONE;
 
   fun is_finite th = case Thm.prop_of th of
-        (_ $ (Const (\<^const_name>\<open>finite\<close>, _) $ A)) => SOME(A,th)
+        (_ $ \<^Const_>\<open>finite _ for A\<close>) => SOME(A,th)
       |  _ => NONE;
 
   fun comb (A,sub_th) (A',fin_th) ths = if A aconv A' then (sub_th,fin_th) :: ths else ths
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Fun.thy
--- a/src/HOL/Fun.thy	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Fun.thy	Wed Aug 07 20:56:31 2024 +0200
@@ -1377,32 +1377,28 @@
 
 simproc_setup fun_upd2 ("f(v := w, x := y)") = \<open>
   let
-    fun gen_fun_upd NONE T _ _ = NONE
-      | gen_fun_upd (SOME f) T x y = SOME (Const (\<^const_name>\<open>fun_upd\<close>, T) $ f $ x $ y)
-    fun dest_fun_T1 (Type (_, T :: Ts)) = T
-    fun find_double (t as Const (\<^const_name>\<open>fun_upd\<close>,T) $ f $ x $ y) =
+    fun gen_fun_upd _ _ _ _ NONE = NONE
+      | gen_fun_upd A B x y (SOME f) = SOME \<^Const>\<open>fun_upd A B for f x y\<close>
+    fun find_double (t as \<^Const_>\<open>fun_upd A B for f x y\<close>) =
       let
-        fun find (Const (\<^const_name>\<open>fun_upd\<close>,T) $ g $ v $ w) =
-              if v aconv x then SOME g else gen_fun_upd (find g) T v w
+        fun find \<^Const_>\<open>fun_upd _ _ for g v w\<close> =
+              if v aconv x then SOME g
+              else gen_fun_upd A B v w (find g)
           | find t = NONE
-      in (dest_fun_T1 T, gen_fun_upd (find f) T x y) end
+      in gen_fun_upd A B x y (find f) end
 
     val ss = simpset_of \<^context>
-
-    fun proc ctxt ct =
-      let
-        val t = Thm.term_of ct
-      in
-        (case find_double t of
-          (T, NONE) => NONE
-        | (T, SOME rhs) =>
-            SOME (Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
-              (fn _ =>
-                resolve_tac ctxt [eq_reflection] 1 THEN
-                resolve_tac ctxt @{thms ext} 1 THEN
-                simp_tac (put_simpset ss ctxt) 1)))
+  in
+    fn _ => fn ctxt => fn ct =>
+      let val t = Thm.term_of ct in
+        find_double t |> Option.map (fn rhs =>
+          Goal.prove ctxt [] [] (Logic.mk_equals (t, rhs))
+            (fn _ =>
+              resolve_tac ctxt [eq_reflection] 1 THEN
+              resolve_tac ctxt @{thms ext} 1 THEN
+              simp_tac (put_simpset ss ctxt) 1))
       end
-  in K proc end
+  end
 \<close>
 
 
diff -r 10c712405854 -r cbfc1058df7c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/HOL.thy	Wed Aug 07 20:56:31 2024 +0200
@@ -818,11 +818,11 @@
 setup \<open>
   (*prevent substitution on bool*)
   let
-    fun non_bool_eq (\<^const_name>\<open>HOL.eq\<close>, Type (_, [T, _])) = T <> \<^typ>\<open>bool\<close>
+    fun non_bool_eq \<^Const_>\<open>HOL.eq T\<close> = T <> \<^Type>\<open>bool\<close>
       | non_bool_eq _ = false;
     fun hyp_subst_tac' ctxt =
       SUBGOAL (fn (goal, i) =>
-        if Term.exists_Const non_bool_eq goal
+        if Term.exists_subterm non_bool_eq goal
         then Hypsubst.hyp_subst_tac ctxt i
         else no_tac);
   in
@@ -1263,7 +1263,7 @@
       | count_loose (s $ t) k = count_loose s k + count_loose t k
       | count_loose (Abs (_, _, t)) k = count_loose  t (k + 1)
       | count_loose _ _ = 0;
-    fun is_trivial_let (Const (\<^const_name>\<open>Let\<close>, _) $ x $ t) =
+    fun is_trivial_let \<^Const_>\<open>Let _ _ for x t\<close> =
       (case t of
         Abs (_, _, t') => count_loose t' 0 <= 1
       | _ => true);
@@ -1277,7 +1277,7 @@
           val (t', ctxt') = yield_singleton (Variable.import_terms false) t ctxt;
         in
           Option.map (hd o Variable.export ctxt' ctxt o single)
-            (case t' of Const (\<^const_name>\<open>Let\<close>,_) $ x $ f => (* x and f are already in normal form *)
+            (case t' of \<^Const_>\<open>Let _ _ for x f\<close> => (* x and f are already in normal form *)
               if is_Free x orelse is_Bound x orelse is_Const x
               then SOME @{thm Let_def}
               else
@@ -1334,26 +1334,28 @@
   "(False \<Longrightarrow> PROP P \<Longrightarrow> PROP Q) \<equiv> (PROP P \<Longrightarrow> False \<Longrightarrow> PROP Q)"
   by (rule swap_prems_eq)
 
-ML \<open>
-fun eliminate_false_implies ct =
+simproc_setup eliminate_false_implies ("False \<Longrightarrow> PROP P") = \<open>
   let
-    val (prems, concl) = Logic.strip_horn (Thm.term_of ct)
-    fun go n =
+    fun conv n =
       if n > 1 then
         Conv.rewr_conv @{thm Pure.swap_prems_eq}
-        then_conv Conv.arg_conv (go (n - 1))
+        then_conv Conv.arg_conv (conv (n - 1))
         then_conv Conv.rewr_conv @{thm HOL.implies_True_equals}
       else
         Conv.rewr_conv @{thm HOL.False_implies_equals}
   in
-    case concl of
-      Const (@{const_name HOL.Trueprop}, _) $ _ => SOME (go (length prems) ct)
-    | _ => NONE
+    fn _ => fn _ => fn ct =>
+      let
+        val t = Thm.term_of ct
+        val n = length (Logic.strip_imp_prems t)
+      in
+        (case Logic.strip_imp_concl t of
+          \<^Const_>\<open>Trueprop for _\<close> => SOME (conv n ct)
+        | _ => NONE)
+      end
   end
 \<close>
 
-simproc_setup eliminate_false_implies ("False \<Longrightarrow> PROP P") = \<open>K (K eliminate_false_implies)\<close>
-
 
 lemma ex_simps:
   "\<And>P Q. (\<exists>x. P x \<and> Q)   = ((\<exists>x. P x) \<and> Q)"
@@ -1536,7 +1538,7 @@
   val rulify = @{thms induct_rulify'}
   val rulify_fallback = @{thms induct_rulify_fallback}
   val equal_def = @{thm induct_equal_def}
-  fun dest_def (Const (\<^const_name>\<open>induct_equal\<close>, _) $ t $ u) = SOME (t, u)
+  fun dest_def \<^Const_>\<open>induct_equal _ for t u\<close> = SOME (t, u)
     | dest_def _ = NONE
   fun trivial_tac ctxt = match_tac ctxt @{thms induct_trueI}
 )
@@ -1937,7 +1939,7 @@
 simproc_setup passive equal (HOL.eq) =
   \<open>fn _ => fn _ => fn ct =>
     (case Thm.term_of ct of
-      Const (_, Type (\<^type_name>\<open>fun\<close>, [Type _, _])) => SOME @{thm eq_equal}
+      \<^Const_>\<open>HOL.eq T\<close> => if is_Type T then SOME @{thm eq_equal} else NONE
     | _ => NONE)\<close>
 
 setup \<open>Code_Preproc.map_pre (fn ctxt => ctxt addsimprocs [\<^simproc>\<open>equal\<close>])\<close>
@@ -2153,7 +2155,7 @@
 ML \<open>
   (* combination of (spec RS spec RS ...(j times) ... spec RS mp) *)
   local
-    fun wrong_prem (Const (\<^const_name>\<open>All\<close>, _) $ Abs (_, _, t)) = wrong_prem t
+    fun wrong_prem \<^Const_>\<open>All _ for \<open>Abs (_, _, t)\<close>\<close> = wrong_prem t
       | wrong_prem (Bound _) = true
       | wrong_prem _ = false;
     val filter_right = filter (not o wrong_prem o HOLogic.dest_Trueprop o hd o Thm.prems_of);
diff -r 10c712405854 -r cbfc1058df7c src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -112,7 +112,7 @@
     : (term list * term list) =
   let
     val Ts = map snd args
-    val ns = Name.variant_list taken (Old_Datatype_Prop.make_tnames Ts)
+    val ns = Name.variant_list taken (Case_Translation.make_tnames Ts)
     val vs = map Free (ns ~~ Ts)
     val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs))
   in
@@ -167,7 +167,7 @@
     fun vars_of args =
       let
         val Ts = map snd args
-        val ns = Old_Datatype_Prop.make_tnames Ts
+        val ns = Case_Translation.make_tnames Ts
       in
         map Free (ns ~~ Ts)
       end
@@ -409,7 +409,7 @@
     val tns = map fst (Term.add_tfreesT lhsT [])
     val resultT = TFree (singleton (Name.variant_list tns) "'t", \<^sort>\<open>pcpo\<close>)
     fun fTs T = map (fn (_, args) => map snd args -->> T) spec
-    val fns = Old_Datatype_Prop.indexify_names (map (K "f") spec)
+    val fns = Case_Translation.indexify_names (map (K "f") spec)
     val fs = map Free (fns ~~ fTs resultT)
     fun caseT T = fTs T -->> (lhsT ->> T)
 
@@ -424,7 +424,7 @@
       fun one_con f (_, args) =
         let
           val Ts = map snd args
-          val ns = Name.variant_list fns (Old_Datatype_Prop.make_tnames Ts)
+          val ns = Name.variant_list fns (Case_Translation.make_tnames Ts)
           val vs = map Free (ns ~~ Ts)
         in
           lambda_args (map fst args ~~ vs) (list_ccomb (f, vs))
@@ -606,7 +606,7 @@
         fun sel_apps_of (i, (con, args: (bool * term option * typ) list)) =
           let
             val Ts : typ list = map #3 args
-            val ns : string list = Old_Datatype_Prop.make_tnames Ts
+            val ns : string list = Case_Translation.make_tnames Ts
             val vs : term list = map Free (ns ~~ Ts)
             val con_app : term = list_ccomb (con, vs)
             val vs' : (bool * term) list = map #1 args ~~ vs
diff -r 10c712405854 -r cbfc1058df7c src/HOL/HOLCF/Tools/Domain/domain_induction.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -63,7 +63,7 @@
       fun prove_take_app (con_const, args) =
         let
           val Ts = map snd args
-          val ns = Name.variant_list ["n"] (Old_Datatype_Prop.make_tnames Ts)
+          val ns = Name.variant_list ["n"] (Case_Translation.make_tnames Ts)
           val vs = map Free (ns ~~ Ts)
           val lhs = mk_capply (take_const $ n', list_ccomb (con_const, vs))
           val rhs = list_ccomb (con_const, map2 (map_of_arg thy) vs Ts)
@@ -108,8 +108,8 @@
   val {take_consts, take_induct_thms, ...} = take_info
 
   val newTs = map #absT iso_infos
-  val P_names = Old_Datatype_Prop.indexify_names (map (K "P") newTs)
-  val x_names = Old_Datatype_Prop.indexify_names (map (K "x") newTs)
+  val P_names = Case_Translation.indexify_names (map (K "P") newTs)
+  val x_names = Case_Translation.indexify_names (map (K "x") newTs)
   val P_types = map (fn T => T --> \<^Type>\<open>bool\<close>) newTs
   val Ps = map Free (P_names ~~ P_types)
   val xs = map Free (x_names ~~ newTs)
@@ -118,7 +118,7 @@
   fun con_assm defined p (con, args) =
     let
       val Ts = map snd args
-      val ns = Name.variant_list P_names (Old_Datatype_Prop.make_tnames Ts)
+      val ns = Name.variant_list P_names (Case_Translation.make_tnames Ts)
       val vs = map Free (ns ~~ Ts)
       val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs))
       fun ind_hyp (v, T) t =
@@ -256,7 +256,7 @@
 
   val {take_consts, take_0_thms, take_lemma_thms, ...} = take_info
 
-  val R_names = Old_Datatype_Prop.indexify_names (map (K "R") newTs)
+  val R_names = Case_Translation.indexify_names (map (K "R") newTs)
   val R_types = map (fn T => T --> T --> \<^Type>\<open>bool\<close>) newTs
   val Rs = map Free (R_names ~~ R_types)
   val n = Free ("n", \<^Type>\<open>nat\<close>)
@@ -273,7 +273,7 @@
     fun one_con T (con, args) =
       let
         val Ts = map snd args
-        val ns1 = Name.variant_list reserved (Old_Datatype_Prop.make_tnames Ts)
+        val ns1 = Name.variant_list reserved (Case_Translation.make_tnames Ts)
         val ns2 = map (fn n => n^"'") ns1
         val vs1 = map Free (ns1 ~~ Ts)
         val vs2 = map Free (ns2 ~~ Ts)
diff -r 10c712405854 -r cbfc1058df7c src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Wed Aug 07 20:56:31 2024 +0200
@@ -422,7 +422,7 @@
     : (term list * term list) =
   let
     val Ts = map snd args;
-    val ns = Name.variant_list taken (Old_Datatype_Prop.make_tnames Ts);
+    val ns = Name.variant_list taken (Case_Translation.make_tnames Ts);
     val vs = map Free (ns ~~ Ts);
     val nonlazy = map snd (filter_out (fst o fst) (args ~~ vs));
   in
@@ -469,10 +469,10 @@
           val Ts = map snd args;
           val Vs =
               (map (K "'t") args)
-              |> Old_Datatype_Prop.indexify_names
+              |> Case_Translation.indexify_names
               |> Name.variant_list tns
               |> map (fn t => TFree (t, \<^sort>\<open>pcpo\<close>));
-          val patNs = Old_Datatype_Prop.indexify_names (map (K "pat") args);
+          val patNs = Case_Translation.indexify_names (map (K "pat") args);
           val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs;
           val pats = map Free (patNs ~~ patTs);
           val fail = mk_fail (mk_tupleT Vs);
@@ -535,10 +535,10 @@
           val Ts = map snd args;
           val Vs =
               (map (K "'t") args)
-              |> Old_Datatype_Prop.indexify_names
+              |> Case_Translation.indexify_names
               |> Name.variant_list (rn::tns)
               |> map (fn t => TFree (t, \<^sort>\<open>pcpo\<close>));
-          val patNs = Old_Datatype_Prop.indexify_names (map (K "pat") args);
+          val patNs = Case_Translation.indexify_names (map (K "pat") args);
           val patTs = map2 (fn T => fn V => T ->> mk_matchT V) Ts Vs;
           val pats = map Free (patNs ~~ patTs);
           val k = Free ("rhs", mk_tupleT Vs ->> R);
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -214,7 +214,7 @@
     val perm_types = map (fn (i, _) =>
       let val T = nth_dtyp i
       in permT --> T --> T end) descr;
-    val perm_names' = Old_Datatype_Prop.indexify_names (map (fn (i, _) =>
+    val perm_names' = Case_Translation.indexify_names (map (fn (i, _) =>
       "perm_" ^ Old_Datatype_Aux.name_of_typ (nth_dtyp i)) descr);
     val perm_names = replicate (length new_type_names) \<^const_name>\<open>Nominal.perm\<close> @
       map (Sign.full_bname thy1) (List.drop (perm_names', length new_type_names));
@@ -226,7 +226,7 @@
       in map (fn (cname, dts) =>
         let
           val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) dts;
-          val names = Name.variant_list ["pi"] (Old_Datatype_Prop.make_tnames Ts);
+          val names = Name.variant_list ["pi"] (Case_Translation.make_tnames Ts);
           val args = map Free (names ~~ Ts);
           val c = Const (cname, Ts ---> T);
           fun perm_arg (dt, x) =
@@ -264,7 +264,7 @@
     val _ = warning ("length descr: " ^ string_of_int (length descr));
     val _ = warning ("length new_type_names: " ^ string_of_int (length new_type_names));
 
-    val perm_indnames = Old_Datatype_Prop.make_tnames (map body_type perm_types);
+    val perm_indnames = Case_Translation.make_tnames (map body_type perm_types);
     val perm_fun_def = Simpdata.mk_eq @{thm perm_fun_def};
 
     val unfolded_perm_eq_thms =
@@ -465,10 +465,10 @@
     val _ = warning "representing sets";
 
     val rep_set_names =
-      Old_Datatype_Prop.indexify_names
+      Case_Translation.indexify_names
         (map (fn (i, _) => Old_Datatype_Aux.name_of_typ (nth_dtyp i) ^ "_set") descr);
     val big_rep_name =
-      space_implode "_" (Old_Datatype_Prop.indexify_names (map_filter
+      space_implode "_" (Case_Translation.indexify_names (map_filter
         (fn (i, (\<^type_name>\<open>noption\<close>, _, _)) => NONE
           | (i, _) => SOME (Old_Datatype_Aux.name_of_typ (nth_dtyp i))) descr)) ^ "_set";
     val _ = warning ("big_rep_name: " ^ big_rep_name);
@@ -1084,7 +1084,7 @@
 
     val _ = warning "proving finite support for the new datatype";
 
-    val indnames = Old_Datatype_Prop.make_tnames recTs;
+    val indnames = Case_Translation.make_tnames recTs;
 
     val abs_supp = Global_Theory.get_thms thy8 "abs_supp";
     val supp_atm = Global_Theory.get_thms thy8 "supp_atm";
@@ -1147,7 +1147,7 @@
     val fsT' = TFree ("'n", \<^sort>\<open>type\<close>);
 
     val fresh_fs = map (fn (s, T) => (T, Free (s, fsT' --> HOLogic.mk_setT T)))
-      (Old_Datatype_Prop.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs);
+      (Case_Translation.indexify_names (replicate (length dt_atomTs) "f") ~~ dt_atomTs);
 
     fun make_pred fsT i T = Free (nth pnames i, fsT --> T --> HOLogic.boolT);
 
@@ -1168,7 +1168,7 @@
         val recs = filter Old_Datatype_Aux.is_rec_type cargs;
         val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr'') cargs;
         val recTs' = map (Old_Datatype_Aux.typ_of_dtyp descr'') recs;
-        val tnames = Name.variant_list pnames (Old_Datatype_Prop.make_tnames Ts);
+        val tnames = Name.variant_list pnames (Case_Translation.make_tnames Ts);
         val rec_tnames = map fst (filter (Old_Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
         val frees = tnames ~~ Ts;
         val frees' = partition_cargs idxs frees;
@@ -1202,7 +1202,7 @@
       map (make_ind_prem fsT (fn T => fn t => fn u =>
         fresh_const T fsT $ t $ u) i T)
           (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs);
-    val tnames = Old_Datatype_Prop.make_tnames recTs;
+    val tnames = Case_Translation.make_tnames recTs;
     val zs = Name.variant_list tnames (replicate (length descr'') "z");
     val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>)
       (map (fn ((((i, _), T), tname), z) =>
@@ -1226,7 +1226,7 @@
     val induct' = Logic.list_implies (ind_prems', ind_concl');
 
     val aux_ind_vars =
-      (Old_Datatype_Prop.indexify_names (replicate (length dt_atomTs) "pi") ~~
+      (Case_Translation.indexify_names (replicate (length dt_atomTs) "pi") ~~
        map mk_permT dt_atomTs) @ [("z", fsT')];
     val aux_ind_Ts = rev (map snd aux_ind_vars);
     val aux_ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>)
@@ -1679,10 +1679,10 @@
     val fun_tuple = foldr1 HOLogic.mk_prod (rec_ctxt :: rec_fns);
     val fun_tupleT = fastype_of fun_tuple;
     val rec_unique_frees =
-      Old_Datatype_Prop.indexify_names (replicate (length recTs) "x") ~~ recTs;
+      Case_Translation.indexify_names (replicate (length recTs) "x") ~~ recTs;
     val rec_unique_frees'' = map (fn (s, T) => (s ^ "'", T)) rec_unique_frees;
     val rec_unique_frees' =
-      Old_Datatype_Prop.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
+      Case_Translation.indexify_names (replicate (length recTs) "y") ~~ rec_result_Ts;
     val rec_unique_concls = map (fn ((x, U), R) =>
         Const (\<^const_name>\<open>Ex1\<close>, (U --> HOLogic.boolT) --> HOLogic.boolT) $
           Abs ("y", U, R $ Free x $ Bound 0))
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -250,7 +250,7 @@
       end) prems);
 
     val ind_vars =
-      (Old_Datatype_Prop.indexify_names (replicate (length atomTs) "pi") ~~
+      (Case_Translation.indexify_names (replicate (length atomTs) "pi") ~~
        map NominalAtoms.mk_permT atomTs) @ [("z", fsT)];
     val ind_Ts = rev (map snd ind_vars);
 
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -267,7 +267,7 @@
       in abs_params params' prem end) prems);
 
     val ind_vars =
-      (Old_Datatype_Prop.indexify_names (replicate (length atomTs) "pi") ~~
+      (Case_Translation.indexify_names (replicate (length atomTs) "pi") ~~
        map NominalAtoms.mk_permT atomTs) @ [("z", fsT)];
     val ind_Ts = rev (map snd ind_vars);
 
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Product_Type.thy	Wed Aug 07 20:56:31 2024 +0200
@@ -1334,22 +1334,22 @@
 simproc_setup Collect_mem ("Collect t") = \<open>
   K (fn ctxt => fn ct =>
     (case Thm.term_of ct of
-      S as Const (\<^const_name>\<open>Collect\<close>, Type (\<^type_name>\<open>fun\<close>, [_, T])) $ t =>
+      S as \<^Const_>\<open>Collect A for t\<close> =>
         let val (u, _, ps) = HOLogic.strip_ptupleabs t in
           (case u of
-            (c as Const (\<^const_name>\<open>Set.member\<close>, _)) $ q $ S' =>
+            (c as \<^Const_>\<open>Set.member _ for q S'\<close>) =>
               (case try (HOLogic.strip_ptuple ps) q of
                 NONE => NONE
               | SOME ts =>
                   if not (Term.is_open S') andalso
                     ts = map Bound (length ps downto 0)
                   then
-                    let val simp =
-                      full_simp_tac (put_simpset HOL_basic_ss ctxt
-                        addsimps [@{thm split_paired_all}, @{thm case_prod_conv}]) 1
+                    let
+                      val simp =
+                        full_simp_tac (put_simpset HOL_basic_ss ctxt
+                          addsimps [@{thm split_paired_all}, @{thm case_prod_conv}]) 1
                     in
-                      SOME (Goal.prove ctxt [] []
-                        (Const (\<^const_name>\<open>Pure.eq\<close>, T --> T --> propT) $ S $ S')
+                      SOME (Goal.prove ctxt [] [] \<^Const>\<open>Pure.eq \<^Type>\<open>set A\<close> for S S'\<close>
                         (K (EVERY
                           [resolve_tac ctxt [eq_reflection] 1,
                            resolve_tac ctxt @{thms subset_antisym} 1,
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Set.thy
--- a/src/HOL/Set.thy	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Set.thy	Wed Aug 07 20:56:31 2024 +0200
@@ -251,7 +251,7 @@
       else raise Match;
 
     fun tr' q = (q, fn _ =>
-      (fn [Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v, Type (\<^type_name>\<open>set\<close>, _)),
+      (fn [Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v, \<^Type>\<open>set _\<close>),
           Const (c, _) $
             (Const (d, _) $ (Const (\<^syntax_const>\<open>_bound\<close>, _) $ Free (v', T)) $ n) $ P] =>
           (case AList.lookup (=) trans (q, c, d) of
diff -r 10c712405854 -r cbfc1058df7c src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -417,9 +417,7 @@
     fold safe_instantiate_bound bindings' ([], HOLogic.dest_Trueprop orig_parent_fmla)
     |> snd (*discard var typing context*)
     |> close_formula
-    |> single
-    |> Type_Infer_Context.infer_types (Context.proof_of (Context.Theory thy))
-    |> the_single
+    |> singleton (Type_Infer_Context.infer_types (Context.proof_of (Context.Theory thy)))
     |> HOLogic.mk_Trueprop
     |> rpair bindings'
   end
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp_grec_sugar.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -1028,8 +1028,7 @@
 
         val deadfixed_T =
           build_map lthy [] [] (mk_undefined o op -->) (apply2 tupleT_of_funT (param1_T, param2_T))
-          |> singleton (Type_Infer_Context.infer_types lthy)
-          |> singleton (Type_Infer.fixate lthy false)
+          |> singleton (Type_Infer_Context.infer_types_finished lthy)
           |> type_of
           |> dest_funT
           |-> generalize_types 1
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -731,7 +731,7 @@
       | rename t _ = t
 
     val (fixed_def_t, _) = yield_singleton (Variable.importT_terms) term ctxt
-    val new_names = Old_Datatype_Prop.make_tnames (all_typs fixed_def_t)
+    val new_names = Case_Translation.make_tnames (all_typs fixed_def_t)
   in
     rename term new_names
   end
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -58,8 +58,8 @@
     lits |> map (atp_literal_of_metis type_enc) |> mk_aconns AOr
 
 fun polish_hol_terms ctxt (lifted, old_skolems) =
-  map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems)
-  #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
+  map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems) #>
+  Type_Infer_Context.infer_types_finished (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
 
 fun hol_clause_of_metis ctxt type_enc sym_tab concealed =
   Metis_Thm.clause
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Tools/Old_Datatype/old_datatype_aux.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_aux.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -157,7 +157,7 @@
   let
     val goal = Thm.term_of cgoal;
     val params = Logic.strip_params goal;
-    val (_, Type (tname, _)) = hd (rev params);
+    val tname = dest_Type_name (#2 (hd (rev params)));
     val exhaustion = Thm.lift_rule cgoal (exh_thm_of tname);
     val prem' = hd (Thm.prems_of exhaustion);
     val _ $ (_ $ lhs $ _) = hd (rev (Logic.strip_assums_hyp prem'));
@@ -228,25 +228,32 @@
 fun mk_fun_dtyp [] U = U
   | mk_fun_dtyp (T :: Ts) U = DtType ("fun", [T, mk_fun_dtyp Ts U]);
 
-fun name_of_typ (Type (s, Ts)) =
-      let val s' = Long_Name.base_name s in
-        space_implode "_"
-          (filter_out (equal "") (map name_of_typ Ts) @
-            [if Symbol_Pos.is_identifier s' then s' else "x"])
-      end
-  | name_of_typ _ = "";
+fun name_of_typ ty =
+  if is_Type ty then
+    let
+      val name = Long_Name.base_name (dest_Type_name ty)
+      val Ts = dest_Type_args ty
+    in
+      space_implode "_"
+        (filter_out (equal "") (map name_of_typ Ts) @
+          [if Symbol_Pos.is_identifier name then name else "x"])
+    end
+  else "";
 
 fun dtyp_of_typ _ (TFree a) = DtTFree a
-  | dtyp_of_typ _ (TVar _) = error "Illegal schematic type variable(s)"
-  | dtyp_of_typ new_dts (Type (tname, Ts)) =
-      (case AList.lookup (op =) new_dts tname of
-        NONE => DtType (tname, map (dtyp_of_typ new_dts) Ts)
-      | SOME vs =>
-          if map (try dest_TFree) Ts = map SOME vs then
-            DtRec (find_index (curry op = tname o fst) new_dts)
-          else error ("Illegal occurrence of recursive type " ^ quote tname));
+  | dtyp_of_typ new_dts T =
+      if is_TVar T then error "Illegal schematic type variable(s)"
+      else
+        let val (tname, Ts) = dest_Type T in
+          (case AList.lookup (op =) new_dts tname of
+            NONE => DtType (tname, map (dtyp_of_typ new_dts) Ts)
+          | SOME vs =>
+              if map (try dest_TFree) Ts = map SOME vs then
+                DtRec (find_index (curry op = tname o fst) new_dts)
+              else error ("Illegal occurrence of recursive type " ^ quote tname))
+        end;
 
-fun typ_of_dtyp descr (DtTFree a) = TFree a
+fun typ_of_dtyp _ (DtTFree a) = TFree a
   | typ_of_dtyp descr (DtRec i) =
       let val (s, ds, _) = the (AList.lookup (op =) descr i)
       in Type (s, map (typ_of_dtyp descr) ds) end
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -15,7 +15,7 @@
   let
     val ctxt = Proof_Context.init_global thy
     val SOME {ctrs, injects, distincts, case_thms, ...} = Ctr_Sugar.ctr_sugar_of ctxt fcT_name
-    val Type (_, As) = body_type (fastype_of (hd ctrs))
+    val As = dest_Type_args (body_type (fastype_of (hd ctrs)))
   in
     Ctr_Sugar_Code.add_ctr_code fcT_name As (map dest_Const ctrs) injects distincts case_thms thy
   end;
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Tools/Old_Datatype/old_datatype_data.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -63,19 +63,17 @@
   let
     val tab = Symtab.lookup_list (#constrs (Data.get thy)) c;
   in
-    (case body_type T of
-      Type (tyco, _) => AList.lookup (op =) tab tyco
-    | _ => NONE)
+    try (dest_Type_name o body_type) T
+    |> Option.mapPartial (AList.lookup (op =) tab)
   end;
 
 fun info_of_constr_permissive thy (c, T) =
   let
     val tab = Symtab.lookup_list (#constrs (Data.get thy)) c;
-    val hint = (case body_type T of Type (tyco, _) => SOME tyco | _ => NONE);
     val default = if null tab then NONE else SOME (snd (List.last tab));
     (*conservative wrt. overloaded constructors*)
   in
-    (case hint of
+    (case try (dest_Type_name o body_type) T of
       NONE => default
     | SOME tyco =>
         (case AList.lookup (op =) tab tyco of
@@ -185,8 +183,9 @@
 
 fun all_distincts thy Ts =
   let
-    fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
-      | add_tycos _ = I;
+    fun add_tycos T =
+      if is_Type T
+      then insert (op =) (dest_Type_name T) #> fold add_tycos (dest_Type_args T) else I;
     val tycos = fold add_tycos Ts [];
   in map_filter (Option.map #distinct o get_info thy) tycos end;
 
@@ -221,7 +220,7 @@
   in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
 
 fun induct_cases descr =
-  Old_Datatype_Prop.indexify_names (maps (dt_cases descr) (map #2 descr));
+  Case_Translation.indexify_names (maps (dt_cases descr) (map #2 descr));
 
 fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
 
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Tools/Old_Datatype/old_datatype_prop.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -7,8 +7,6 @@
 signature OLD_DATATYPE_PROP =
 sig
   type descr = Old_Datatype_Aux.descr
-  val indexify_names: string list -> string list
-  val make_tnames: typ list -> string list
   val make_injs : descr list -> term list list
   val make_distincts : descr list -> term list list (*no symmetric inequalities*)
   val make_ind : descr list -> term
@@ -29,18 +27,6 @@
 type descr = Old_Datatype_Aux.descr;
 
 
-val indexify_names = Case_Translation.indexify_names;
-val make_tnames = Case_Translation.make_tnames;
-
-fun make_tnames Ts =
-  let
-    fun type_name (TFree (name, _)) = unprefix "'" name
-      | type_name (Type (name, _)) =
-          let val name' = Long_Name.base_name name
-          in if Symbol_Pos.is_identifier name' then name' else "x" end;
-  in indexify_names (map type_name Ts) end;
-
-
 (************************* injectivity of constructors ************************)
 
 fun make_injs descr =
@@ -52,7 +38,7 @@
         let
           val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
           val constr_t = Const (cname, Ts ---> T);
-          val tnames = make_tnames Ts;
+          val tnames = Case_Translation.make_tnames Ts;
           val frees = map Free (tnames ~~ Ts);
           val frees' = map Free (map (suffix "'") tnames ~~ Ts);
         in
@@ -80,12 +66,13 @@
     fun make_distincts' _ [] = []
       | make_distincts' T ((cname, cargs) :: constrs) =
           let
-            val frees = map Free (make_tnames cargs ~~ cargs);
+            val frees = map Free (Case_Translation.make_tnames cargs ~~ cargs);
             val t = list_comb (Const (cname, cargs ---> T), frees);
 
             fun make_distincts'' (cname', cargs') =
               let
-                val frees' = map Free (map (suffix "'") (make_tnames cargs') ~~ cargs');
+                val frees' =
+                  map Free (map (suffix "'") (Case_Translation.make_tnames cargs') ~~ cargs');
                 val t' = list_comb (Const (cname', cargs' ---> T), frees');
               in
                 HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.mk_eq (t, t'))
@@ -107,9 +94,7 @@
       if length descr' = 1 then ["P"]
       else map (fn i => "P" ^ string_of_int i) (1 upto length descr');
 
-    fun make_pred i T =
-      let val T' = T --> HOLogic.boolT
-      in Free (nth pnames i, T') end;
+    fun make_pred i T = Free (nth pnames i, T --> \<^Type>\<open>bool\<close>);
 
     fun make_ind_prem k T (cname, cargs) =
       let
@@ -125,7 +110,7 @@
         val recs = filter Old_Datatype_Aux.is_rec_type cargs;
         val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
         val recTs' = map (Old_Datatype_Aux.typ_of_dtyp descr') recs;
-        val tnames = Name.variant_list pnames (make_tnames Ts);
+        val tnames = Name.variant_list pnames (Case_Translation.make_tnames Ts);
         val rec_tnames = map fst (filter (Old_Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
         val frees = tnames ~~ Ts;
         val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
@@ -138,7 +123,7 @@
 
     val prems =
       maps (fn ((i, (_, _, constrs)), T) => map (make_ind_prem i T) constrs) (descr' ~~ recTs);
-    val tnames = make_tnames recTs;
+    val tnames = Case_Translation.make_tnames recTs;
     val concl =
       HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop \<^const_name>\<open>HOL.conj\<close>)
         (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T))
@@ -155,18 +140,18 @@
     fun make_casedist_prem T (cname, cargs) =
       let
         val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
-        val frees = Name.variant_list ["P", "y"] (make_tnames Ts) ~~ Ts;
+        val frees = Name.variant_list ["P", "y"] (Case_Translation.make_tnames Ts) ~~ Ts;
         val free_ts = map Free frees;
       in
         fold_rev (Logic.all o Free) frees
           (Logic.mk_implies (HOLogic.mk_Trueprop
             (HOLogic.mk_eq (Free ("y", T), list_comb (Const (cname, Ts ---> T), free_ts))),
-              HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))))
+              HOLogic.mk_Trueprop (Free ("P", \<^Type>\<open>bool\<close>))))
       end;
 
     fun make_casedist ((_, (_, _, constrs))) T =
       let val prems = map (make_casedist_prem T) constrs
-      in Logic.list_implies (prems, HOLogic.mk_Trueprop (Free ("P", HOLogic.boolT))) end;
+      in Logic.list_implies (prems, HOLogic.mk_Trueprop (Free ("P", \<^Type>\<open>bool\<close>))) end;
 
   in
     map2 make_casedist (hd descr)
@@ -219,7 +204,7 @@
         val recs = filter Old_Datatype_Aux.is_rec_type cargs;
         val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
         val recTs' = map (Old_Datatype_Aux.typ_of_dtyp descr') recs;
-        val tnames = make_tnames Ts;
+        val tnames = Case_Translation.make_tnames Ts;
         val rec_tnames = map fst (filter (Old_Datatype_Aux.is_rec_type o snd) (tnames ~~ cargs));
         val frees = map Free (tnames ~~ Ts);
         val frees' = map Free (rec_tnames ~~ recTs');
@@ -276,7 +261,7 @@
     fun make_case T comb_t ((cname, cargs), f) =
       let
         val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
-        val frees = map Free ((make_tnames Ts) ~~ Ts);
+        val frees = map Free ((Case_Translation.make_tnames Ts) ~~ Ts);
       in
         HOLogic.mk_Trueprop
           (HOLogic.mk_eq (comb_t $ list_comb (Const (cname, Ts ---> T), frees),
@@ -298,7 +283,7 @@
     val used' = fold Term.add_tfree_namesT recTs [];
     val newTs = take (length (hd descr)) recTs;
     val T' = TFree (singleton (Name.variant_list used') "'t", \<^sort>\<open>type\<close>);
-    val P = Free ("P", T' --> HOLogic.boolT);
+    val P = Free ("P", T' --> \<^Type>\<open>bool\<close>);
 
     fun make_split (((_, (_, _, constrs)), T), comb_t) =
       let
@@ -308,7 +293,7 @@
         fun process_constr ((cname, cargs), f) (t1s, t2s) =
           let
             val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
-            val frees = map Free (Name.variant_list used (make_tnames Ts) ~~ Ts);
+            val frees = map Free (Name.variant_list used (Case_Translation.make_tnames Ts) ~~ Ts);
             val eqn = HOLogic.mk_eq (Free ("x", T), list_comb (Const (cname, Ts ---> T), frees));
             val P' = P $ list_comb (f, frees);
           in
@@ -337,7 +322,7 @@
 
     fun mk_case_cong comb =
       let
-        val Type ("fun", [T, _]) = fastype_of comb;
+        val \<^Type>\<open>fun T _\<close> = fastype_of comb;
         val M = Free ("M", T);
         val M' = Free ("M'", T);
       in
@@ -367,7 +352,7 @@
 
     fun mk_case_cong ((comb, comb'), (_, (_, _, constrs))) =
       let
-        val Type ("fun", [T, _]) = fastype_of comb;
+        val \<^Type>\<open>fun T _\<close> = fastype_of comb;
         val (_, fs) = strip_comb comb;
         val (_, gs) = strip_comb comb';
         val used = ["M", "M'"] @ map (fst o dest_Free) (fs @ gs);
@@ -377,7 +362,7 @@
         fun mk_clause ((f, g), (cname, _)) =
           let
             val Ts = binder_types (fastype_of f);
-            val tnames = Name.variant_list used (make_tnames Ts);
+            val tnames = Name.variant_list used (Case_Translation.make_tnames Ts);
             val frees = map Free (tnames ~~ Ts);
           in
             fold_rev Logic.all frees
@@ -411,7 +396,7 @@
     fun mk_eqn T (cname, cargs) =
       let
         val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
-        val tnames = Name.variant_list ["v"] (make_tnames Ts);
+        val tnames = Name.variant_list ["v"] (Case_Translation.make_tnames Ts);
         val frees = tnames ~~ Ts;
       in
         fold_rev (fn (s, T') => fn t => HOLogic.mk_exists (s, T', t)) frees
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Tools/Old_Datatype/old_primrec.ML
--- a/src/HOL/Tools/Old_Datatype/old_primrec.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_primrec.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -144,7 +144,7 @@
       (case AList.lookup (op =) eqns cname of
         NONE => (warning ("No equation for constructor " ^ quote cname ^
           "\nin definition of function " ^ quote fname);
-            (fnames', fnss', (Const (\<^const_name>\<open>undefined\<close>, dummyT)) :: fns))
+            (fnames', fnss', \<^Const>\<open>undefined dummyT\<close> :: fns))
       | SOME (ls, cargs', rs, rhs, eq) =>
           let
             val recs = filter (Old_Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs);
@@ -183,9 +183,9 @@
   (case AList.lookup (op =) fns i of
     NONE =>
       let
-        val dummy_fns = map (fn (_, cargs) => Const (\<^const_name>\<open>undefined\<close>,
-          replicate (length cargs + length (filter Old_Datatype_Aux.is_rec_type cargs))
-            dummyT ---> HOLogic.unitT)) constrs;
+        val dummy_fns = map (fn (_, cargs) => \<^Const>\<open>undefined
+          \<open>replicate (length cargs + length (filter Old_Datatype_Aux.is_rec_type cargs))
+            dummyT ---> HOLogic.unitT\<close>\<close>) constrs;
         val _ = warning ("No function definition for datatype " ^ quote tname)
       in
         (dummy_fns @ fs, defs)
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Tools/Old_Datatype/old_rep_datatype.ML
--- a/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_rep_datatype.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -40,11 +40,10 @@
 
     fun prove_casedist_thm (i, (T, t)) =
       let
-        val dummyPs = map (fn (Var (_, Type (_, [T', T'']))) =>
-          Abs ("z", T', Const (\<^const_name>\<open>True\<close>, T''))) induct_Ps;
+        val dummyPs = map (fn Var (_, \<^Type>\<open>fun A _\<close>) => Abs ("z", A, \<^Const>\<open>True\<close>)) induct_Ps;
         val P =
           Abs ("z", T, HOLogic.imp $ HOLogic.mk_eq (Var (("a", maxidx + 1), T), Bound 0) $
-            Var (("P", 0), HOLogic.boolT));
+            Var (("P", 0), \<^Type>\<open>bool\<close>));
         val insts = take i dummyPs @ (P :: drop (i + 1) dummyPs);
       in
         Goal.prove_sorry_global thy []
@@ -102,7 +101,7 @@
     val (rec_result_Ts, reccomb_fn_Ts) = Old_Datatype_Prop.make_primrec_Ts descr used;
 
     val rec_set_Ts =
-      map (fn (T1, T2) => (reccomb_fn_Ts @ [T1, T2]) ---> HOLogic.boolT) (recTs ~~ rec_result_Ts);
+      map (fn (T1, T2) => (reccomb_fn_Ts @ [T1, T2]) ---> \<^Type>\<open>bool\<close>) (recTs ~~ rec_result_Ts);
 
     val rec_fns =
       map (uncurry (Old_Datatype_Aux.mk_Free "f")) (reccomb_fn_Ts ~~ (1 upto length reccomb_fn_Ts));
@@ -204,8 +203,8 @@
       let
         val rec_unique_ts =
           map (fn (((set_t, T1), T2), i) =>
-            Const (\<^const_name>\<open>Ex1\<close>, (T2 --> HOLogic.boolT) --> HOLogic.boolT) $
-              absfree ("y", T2) (set_t $ Old_Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2)))
+            \<^Const>\<open>Ex1 T2 for
+              \<open>absfree ("y", T2) (set_t $ Old_Datatype_Aux.mk_Free "x" T1 i $ Free ("y", T2))\<close>\<close>)
                 (rec_sets ~~ recTs ~~ rec_result_Ts ~~ (1 upto length recTs));
         val insts =
           map (fn ((i, T), t) => absfree ("x" ^ string_of_int i, T) t)
@@ -248,8 +247,7 @@
             (fn ((((name, comb), set), T), T') =>
               (Binding.name (Thm.def_name (Long_Name.base_name name)),
                 Logic.mk_equals (comb, fold_rev lambda rec_fns (absfree ("x", T)
-                 (Const (\<^const_name>\<open>The\<close>, (T' --> HOLogic.boolT) --> T') $ absfree ("y", T')
-                   (set $ Free ("x", T) $ Free ("y", T')))))))
+                 \<^Const>\<open>The T' for \<open>absfree ("y", T') (set $ Free ("x", T) $ Free ("y", T'))\<close>\<close>))))
             (reccomb_names ~~ reccombs ~~ rec_sets ~~ recTs ~~ rec_result_Ts))
       ||> Sign.parent_path;
 
@@ -303,43 +301,45 @@
         let
           val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
           val Ts' = map mk_dummyT (filter Old_Datatype_Aux.is_rec_type cargs)
-        in Const (\<^const_name>\<open>undefined\<close>, Ts @ Ts' ---> T') end) constrs) descr';
+        in \<^Const>\<open>undefined \<open>Ts @ Ts' ---> T'\<close>\<close> end) constrs) descr';
 
     val case_names0 = map (fn s => Sign.full_bname thy1 ("case_" ^ s)) new_type_names;
 
     (* define case combinators via primrec combinators *)
 
-    fun def_case ((((i, (_, _, constrs)), T as Type (Tcon, _)), name), recname) (defs, thy) =
-      if is_some (Ctr_Sugar.ctr_sugar_of ctxt Tcon) then
-        (defs, thy)
-      else
-        let
-          val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
-            let
-              val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
-              val Ts' = Ts @ map mk_dummyT (filter Old_Datatype_Aux.is_rec_type cargs);
-              val frees' = map2 (Old_Datatype_Aux.mk_Free "x") Ts' (1 upto length Ts');
-              val frees = take (length cargs) frees';
-              val free = Old_Datatype_Aux.mk_Free "f" (Ts ---> T') j;
-            in
-              (free, fold_rev (absfree o dest_Free) frees' (list_comb (free, frees)))
-            end) (constrs ~~ (1 upto length constrs)));
+    fun def_case ((((i, (_, _, constrs)), T), name), recname) (defs, thy) =
+      let val Tcon = dest_Type_name T in
+        if is_some (Ctr_Sugar.ctr_sugar_of ctxt Tcon) then
+          (defs, thy)
+        else
+          let
+            val (fns1, fns2) = split_list (map (fn ((_, cargs), j) =>
+              let
+                val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr') cargs;
+                val Ts' = Ts @ map mk_dummyT (filter Old_Datatype_Aux.is_rec_type cargs);
+                val frees' = map2 (Old_Datatype_Aux.mk_Free "x") Ts' (1 upto length Ts');
+                val frees = take (length cargs) frees';
+                val free = Old_Datatype_Aux.mk_Free "f" (Ts ---> T') j;
+              in
+                (free, fold_rev (absfree o dest_Free) frees' (list_comb (free, frees)))
+              end) (constrs ~~ (1 upto length constrs)));
 
-          val caseT = map (snd o dest_Free) fns1 @ [T] ---> T';
-          val fns = flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns);
-          val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
-          val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
-          val def =
-            (Binding.name (Thm.def_name (Long_Name.base_name name)),
-              Logic.mk_equals (Const (name, caseT),
-                fold_rev lambda fns1
-                  (list_comb (reccomb,
-                    flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns)))));
-          val (def_thm, thy') =
-            thy
-            |> Sign.declare_const_global decl |> snd
-            |> Global_Theory.add_def def;
-        in (defs @ [def_thm], thy') end;
+            val caseT = map (snd o dest_Free) fns1 @ [T] ---> T';
+            val fns = flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns);
+            val reccomb = Const (recname, (map fastype_of fns) @ [T] ---> T');
+            val decl = ((Binding.name (Long_Name.base_name name), caseT), NoSyn);
+            val def =
+              (Binding.name (Thm.def_name (Long_Name.base_name name)),
+                Logic.mk_equals (Const (name, caseT),
+                  fold_rev lambda fns1
+                    (list_comb (reccomb,
+                      flat (take i case_dummy_fns) @ fns2 @ flat (drop (i + 1) case_dummy_fns)))));
+            val (def_thm, thy') =
+              thy
+              |> Sign.declare_const_global decl |> snd
+              |> Global_Theory.add_def def;
+          in (defs @ [def_thm], thy') end
+      end;
 
     val (case_defs, thy2) =
       fold def_case (hd descr ~~ newTs ~~ case_names0 ~~ take (length newTs) reccomb_names)
@@ -350,8 +350,8 @@
         EVERY [rewrite_goals_tac ctxt (case_defs @ map mk_meta_eq primrec_thms),
           resolve_tac ctxt [refl] 1]);
 
-    fun prove_cases (Type (Tcon, _)) ts =
-      (case Ctr_Sugar.ctr_sugar_of ctxt Tcon of
+    fun prove_cases T ts =
+      (case Ctr_Sugar.ctr_sugar_of ctxt (dest_Type_name T) of
         SOME {case_thms, ...} => case_thms
       | NONE => map prove_case ts);
 
@@ -455,8 +455,8 @@
   let
     fun prove_case_cong ((t, nchotomy), case_rewrites) =
       let
-        val Const (\<^const_name>\<open>Pure.imp\<close>, _) $ tm $ _ = t;
-        val Const (\<^const_name>\<open>Trueprop\<close>, _) $ (Const (\<^const_name>\<open>HOL.eq\<close>, _) $ _ $ Ma) = tm;
+        val \<^Const_>\<open>Pure.imp for tm _\<close> = t;
+        val \<^Const_>\<open>Trueprop for \<^Const_>\<open>HOL.eq _ for _ Ma\<close>\<close> = tm;
         val nchotomy' = nchotomy RS spec;
         val [v] = Term.add_var_names (Thm.concl_of nchotomy') [];
       in
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Tools/SMT/smtlib_proof.ML
--- a/src/HOL/Tools/SMT/smtlib_proof.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/SMT/smtlib_proof.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -97,9 +97,7 @@
 
     val needs_inferT = equal Term.dummyT orf Term.is_TVar
     val needs_infer = Term.exists_type (Term.exists_subtype needs_inferT)
-    fun infer_types ctxt =
-      singleton (Type_Infer_Context.infer_types ctxt) #>
-      singleton (Proof_Context.standard_term_check_finish ctxt)
+    fun infer_types ctxt = singleton (Type_Infer_Context.infer_types_finished ctxt)
     fun infer ctxt t = if needs_infer t then infer_types ctxt t else t
 
     val (t, {ctxt = ctxt', extra = names, ...}: ((string * (string * typ)) list, 'b) context) =
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/datatype_realizer.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -49,7 +49,7 @@
       (fn ((i, (_, _, constrs)), T) => fold_map (fn (cname, cargs) => fn j =>
         let
           val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
-          val tnames = Name.variant_list pnames (Old_Datatype_Prop.make_tnames Ts);
+          val tnames = Name.variant_list pnames (Case_Translation.make_tnames Ts);
           val recs = filter (Old_Datatype_Aux.is_rec_type o fst o fst) (cargs ~~ tnames ~~ Ts);
           val frees = tnames ~~ Ts;
 
@@ -88,7 +88,7 @@
           else if (j: int) = i then HOLogic.mk_fst t
           else mk_proj j is (HOLogic.mk_snd t);
 
-    val tnames = Old_Datatype_Prop.make_tnames recTs;
+    val tnames = Case_Translation.make_tnames recTs;
     val fTs = map fastype_of rec_fns;
     val ps = map (fn ((((i, _), T), U), s) => Abs ("x", T, make_pred i U T
       (list_comb (Const (s, fTs ---> T --> U), rec_fns) $ Bound 0) (Bound 0)))
@@ -168,7 +168,7 @@
     fun make_casedist_prem T (cname, cargs) =
       let
         val Ts = map (Old_Datatype_Aux.typ_of_dtyp descr) cargs;
-        val frees = Name.variant_list ["P", "y"] (Old_Datatype_Prop.make_tnames Ts) ~~ Ts;
+        val frees = Name.variant_list ["P", "y"] (Case_Translation.make_tnames Ts) ~~ Ts;
         val free_ts = map Free frees;
         val r = Free ("r" ^ Long_Name.base_name cname, Ts ---> rT)
       in
diff -r 10c712405854 -r cbfc1058df7c src/HOL/Tools/set_comprehension_pointfree.ML
--- a/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/HOL/Tools/set_comprehension_pointfree.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -461,21 +461,16 @@
     |> Option.map (fn thm => thm RS @{thm eq_reflection})
   end;
 
-fun instantiate_arg_cong ctxt pred =
-  let
-    val arg_cong = Thm.incr_indexes (maxidx_of_term pred + 1) @{thm arg_cong}
-    val (Var (f, _) $ _, _) = HOLogic.dest_eq (HOLogic.dest_Trueprop (Thm.concl_of arg_cong))
-  in
-    infer_instantiate ctxt [(f, Thm.cterm_of ctxt pred)] arg_cong
-  end;
-
 fun proc ctxt redex =
   let
-    val pred $ set_compr = Thm.term_of redex
-    val arg_cong' = instantiate_arg_cong ctxt pred
+    val (f, set_compr) = Thm.dest_comb redex
+    val [A, B] = Thm.dest_ctyp (Thm.ctyp_of_cterm f)
+    val cong =
+      \<^instantiate>\<open>'a = A and 'b = B and f
+        in lemma (schematic) "x = y \<Longrightarrow> f x \<equiv> f y" by simp\<close>
   in
-    conv ctxt set_compr
-    |> Option.map (fn thm => thm RS arg_cong' RS @{thm eq_reflection})
+    conv ctxt (Thm.term_of set_compr)
+    |> Option.map (fn thm => thm RS cong)
   end;
 
 fun code_proc ctxt redex =
diff -r 10c712405854 -r cbfc1058df7c src/Provers/splitter.ML
--- a/src/Provers/splitter.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/Provers/splitter.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -428,9 +428,12 @@
 
 (* add_split / del_split *)
 
-fun string_of_typ (Type (s, Ts)) =
-      (if null Ts then "" else enclose "(" ")" (commas (map string_of_typ Ts))) ^ s
-  | string_of_typ _ = "_";
+fun string_of_typ T =
+  if is_Type T then
+    (case dest_Type_args T of
+      [] => ""
+    | Ts => enclose "(" ")" (commas (map string_of_typ Ts))) ^ dest_Type_name T
+  else "_";
 
 fun split_name (name, T) asm = "split " ^
   (if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T;
diff -r 10c712405854 -r cbfc1058df7c src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Wed Aug 07 20:56:31 2024 +0200
@@ -16,7 +16,7 @@
 object Isabelle_Cronjob {
   /* global resources: owned by main cronjob */
 
-  val backup = "lxbroy10:cronjob"
+  val backup = "isabelle.in.tum.de:cronjob"
   val main_dir: Path = Path.explode("~/cronjob")
   val main_state_file: Path = main_dir + Path.explode("run/main.state")
   val build_release_log: Path = main_dir + Path.explode("run/build_release.log")
diff -r 10c712405854 -r cbfc1058df7c src/Pure/type_infer_context.ML
--- a/src/Pure/type_infer_context.ML	Wed Aug 07 12:39:09 2024 +0100
+++ b/src/Pure/type_infer_context.ML	Wed Aug 07 20:56:31 2024 +0200
@@ -11,6 +11,7 @@
   val prepare_positions: Proof.context -> term list -> term list * (Position.T * typ) list
   val prepare: Proof.context -> term list -> int * term list
   val infer_types: Proof.context -> term list -> term list
+  val infer_types_finished: Proof.context -> term list -> term list
 end;
 
 structure Type_Infer_Context: TYPE_INFER_CONTEXT =
@@ -304,4 +305,7 @@
     val (_, ts') = Type_Infer.finish ctxt tye ([], ts);
   in ts' end;
 
+fun infer_types_finished ctxt =
+  infer_types ctxt #> Proof_Context.standard_term_check_finish ctxt;
+
 end;