author | wenzelm |
Wed, 07 Aug 2024 13:54:09 +0200 | |
changeset 80660 | c8c13c5e408f |
parent 80659 | 2191ad2d684e |
child 80661 | 231d58c412b5 |
--- 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 ************************)