src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML
changeset 42761 8ea9c6fa8b53
parent 42755 4603154a3018
child 42778 896aaab98563
equal deleted inserted replaced
42760:d83802e7348e 42761:8ea9c6fa8b53
   267 (* This shouldn't clash with anything else. *)
   267 (* This shouldn't clash with anything else. *)
   268 val mangled_type_sep = "\000"
   268 val mangled_type_sep = "\000"
   269 
   269 
   270 fun generic_mangled_type_name f (ATerm (name, [])) = f name
   270 fun generic_mangled_type_name f (ATerm (name, [])) = f name
   271   | generic_mangled_type_name f (ATerm (name, tys)) =
   271   | generic_mangled_type_name f (ATerm (name, tys)) =
   272     f name ^ "(" ^ commas (map (generic_mangled_type_name f) tys) ^ ")"
   272     f name ^ "(" ^ space_implode "," (map (generic_mangled_type_name f) tys)
       
   273     ^ ")"
   273 val mangled_type_name =
   274 val mangled_type_name =
   274   fo_term_from_typ
   275   fo_term_from_typ
   275   #> (fn ty => (make_tff_type (generic_mangled_type_name fst ty),
   276   #> (fn ty => (make_tff_type (generic_mangled_type_name fst ty),
   276                 generic_mangled_type_name snd ty))
   277                 generic_mangled_type_name snd ty))
   277 
   278