--- 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;