diff -r f6d9e0e0b153 -r 1de908189869 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Wed Dec 03 21:00:39 2008 -0800
+++ b/src/HOL/Import/proof_kernel.ML	Thu Dec 04 14:43:33 2008 +0100
@@ -1960,7 +1960,7 @@
         val hth = case Shuffler.set_prop thy22 (HOLogic.mk_Trueprop tm24) [("",th)] of
                       SOME (_,res) => HOLThm(rens_of linfo,res)
                     | NONE => raise ERR "new_definition" "Bad conclusion"
-        val fullname = Sign.full_name thy22 thmname
+        val fullname = Sign.full_bname thy22 thmname
         val thy22' = case opt_get_output_thy thy22 of
                          "" => (ImportRecorder.add_hol_mapping thyname thmname fullname;
                                 add_hol4_mapping thyname thmname fullname thy22)