# HG changeset patch # User wenzelm # Date 1723040814 -7200 # Node ID 477ca08c9091c26237b058ac790ad50be653bfd9 # Parent 86b4d400da38ecbe51630ccf41a0bfb6f0cf992c tuned: more abstract access to datatype typ; diff -r 86b4d400da38 -r 477ca08c9091 src/Provers/splitter.ML --- a/src/Provers/splitter.ML Wed Aug 07 15:37:27 2024 +0200 +++ b/src/Provers/splitter.ML Wed Aug 07 16:26:54 2024 +0200 @@ -428,9 +428,12 @@ (* add_split / del_split *) -fun string_of_typ (Type (s, Ts)) = - (if null Ts then "" else enclose "(" ")" (commas (map string_of_typ Ts))) ^ s - | string_of_typ _ = "_"; +fun string_of_typ T = + if is_Type T then + (case dest_Type_args T of + [] => "" + | Ts => enclose "(" ")" (commas (map string_of_typ Ts))) ^ dest_Type_name T + else "_"; fun split_name (name, T) asm = "split " ^ (if asm then "asm " else "") ^ name ^ " :: " ^ string_of_typ T;