--- 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)