removed odd clone (amending 100c0eaf63d5);
authorwenzelm
Wed, 07 Aug 2024 13:54:09 +0200
changeset 80660 c8c13c5e408f
parent 80659 2191ad2d684e
child 80661 231d58c412b5
removed odd clone (amending 100c0eaf63d5); NB: Case_Translation.make_tnames covers TVar case as well, but this is not relevant here;
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 ************************)