src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42761 8ea9c6fa8b53
parent 42755 4603154a3018
child 42778 896aaab98563
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML	Thu May 12 15:29:19 2011 +0200
@@ -269,7 +269,8 @@
 
 fun generic_mangled_type_name f (ATerm (name, [])) = f name
   | generic_mangled_type_name f (ATerm (name, tys)) =
-    f name ^ "(" ^ commas (map (generic_mangled_type_name f) tys) ^ ")"
+    f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
+    ^ ")"
 val mangled_type_name =
   fo_term_from_typ
   #> (fn ty => (make_tff_type (generic_mangled_type_name fst ty),