src/HOL/TPTP/TPTP_Proof_Reconstruction.thy

 
     val def_name = const_name ^ "_def"
 
     val bnd_def = (*FIXME consts*)
       const_name
-      |> space_implode "." o tl o space_explode "." (*FIXME hack to drop theory-name prefix*)
+      |> Long_Name.implode o tl o Long_Name.explode (*FIXME hack to drop theory-name prefix*)
       |> Binding.qualified_name
       |> Binding.suffix_name "_def"
 
     val bnd_name =
       case prob_name_opt of