tuned: more abstract access to datatype typ;
authorwenzelm
Wed, 07 Aug 2024 16:26:54 +0200
changeset 80664 477ca08c9091
parent 80663 86b4d400da38
child 80665 294f3734411c
tuned: more abstract access to datatype typ;
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;