src/HOL/Import/proof_kernel.ML

         val thy'' = add_hol4_const_mapping thyname constname true fullcname thy'
         val _ = ImportRecorder.add_hol_const_mapping thyname constname fullcname
         val (linfo,tm24) = disamb_term (mk_teq constname rhs' thy'')
         val rew = rewrite_hol4_term eq thy''
         val crhs = cterm_of thy'' (#2 (Logic.dest_equals (prop_of rew)))
-        val thy22 = if (def_name constname) = thmname andalso not redeclared andalso csyn = NoSyn
+        val thy22 = if Thm.def_name constname = thmname andalso not redeclared andalso csyn = NoSyn
                     then
                         let
                             val p1 = quotename constname
                             val p2 = Display.string_of_ctyp (ctyp_of thy'' ctype)
                             val p3 = string_of_mixfix csyn

             val hth = HOLThm(rens,res')
             val rew = rewrite_hol4_term (concl_of res') thy'
             val th  = equal_elim rew res'
             fun handle_const (name,thy) =
                 let
-                    val defname = def_name name
+                    val defname = Thm.def_name name
                     val (newname,thy') = get_defname thyname name thy
                 in
                     (if defname = newname
                      then quotename name
                      else (quotename newname) ^ ": " ^ (quotename name),thy')