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