# HG changeset patch
# User wenzelm
# Date 1723031649 -7200
# Node ID c8c13c5e408fa8e4a65b5be122ea8d599a700edb
# Parent  2191ad2d684e2db917ddee4ae31d92a2aedba26e
removed odd clone (amending 100c0eaf63d5);
NB: Case_Translation.make_tnames covers TVar case as well, but this is not relevant here;

diff -r 2191ad2d684e -r c8c13c5e408f src/HOL/Tools/Old_Datatype/old_datatype_prop.ML
--- 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 ************************)