# HG changeset patch
# User wenzelm
# Date 1723034691 -7200
# Node ID 231d58c412b53f0b2f4b276abe5ac5688bc300e7
# Parent  c8c13c5e408fa8e4a65b5be122ea8d599a700edb
tuned signature: eliminate aliases;

diff -r c8c13c5e408f -r 231d58c412b5 src/HOL/HOLCF/Tools/Domain/domain_constructors.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_constructors.ML	Wed Aug 07 14:44:51 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 c8c13c5e408f -r 231d58c412b5 src/HOL/HOLCF/Tools/Domain/domain_induction.ML
--- a/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/HOLCF/Tools/Domain/domain_induction.ML	Wed Aug 07 14:44:51 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 c8c13c5e408f -r 231d58c412b5 src/HOL/HOLCF/ex/Pattern_Match.thy
--- a/src/HOL/HOLCF/ex/Pattern_Match.thy	Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/HOLCF/ex/Pattern_Match.thy	Wed Aug 07 14:44:51 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 c8c13c5e408f -r 231d58c412b5 src/HOL/Nominal/nominal_datatype.ML
--- a/src/HOL/Nominal/nominal_datatype.ML	Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML	Wed Aug 07 14:44:51 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 c8c13c5e408f -r 231d58c412b5 src/HOL/Nominal/nominal_inductive.ML
--- a/src/HOL/Nominal/nominal_inductive.ML	Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/Nominal/nominal_inductive.ML	Wed Aug 07 14:44:51 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 c8c13c5e408f -r 231d58c412b5 src/HOL/Nominal/nominal_inductive2.ML
--- a/src/HOL/Nominal/nominal_inductive2.ML	Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/Nominal/nominal_inductive2.ML	Wed Aug 07 14:44:51 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 c8c13c5e408f -r 231d58c412b5 src/HOL/Tools/Lifting/lifting_def_code_dt.ML
--- a/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def_code_dt.ML	Wed Aug 07 14:44:51 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 c8c13c5e408f -r 231d58c412b5 src/HOL/Tools/Old_Datatype/old_datatype_data.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Wed Aug 07 14:44:51 2024 +0200
@@ -220,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 c8c13c5e408f -r 231d58c412b5 src/HOL/Tools/Old_Datatype/old_datatype_prop.ML
--- a/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML	Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML	Wed Aug 07 14:44:51 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
@@ -28,9 +26,6 @@
 
 type descr = Old_Datatype_Aux.descr;
 
-val indexify_names = Case_Translation.indexify_names;
-val make_tnames = Case_Translation.make_tnames;
-
 
 (************************* injectivity of constructors ************************)
 
@@ -43,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
@@ -71,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'))
@@ -114,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');
@@ -127,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))
@@ -144,7 +140,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"] (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
@@ -208,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');
@@ -265,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),
@@ -297,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
@@ -366,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
@@ -400,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 c8c13c5e408f -r 231d58c412b5 src/HOL/Tools/datatype_realizer.ML
--- a/src/HOL/Tools/datatype_realizer.ML	Wed Aug 07 13:54:09 2024 +0200
+++ b/src/HOL/Tools/datatype_realizer.ML	Wed Aug 07 14:44:51 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