diff -r bf80d125406b -r 4c43a2881b25 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Mar 19 21:59:31 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Wed Mar 19 22:10:33 2014 +0100
@@ -722,7 +722,7 @@
 
     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"