removed odd clone (amending 100c0eaf63d5);
NB: Case_Translation.make_tnames covers TVar case as well, but this is not relevant here;
--- a/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML Wed Aug 07 13:45:37 2024 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_prop.ML Wed Aug 07 13:54:09 2024 +0200
@@ -28,18 +28,9 @@
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 ************************)