# HG changeset patch
# User wenzelm
# Date 1224768519 -7200
# Node ID 4693938e9c2a5d6db997ee5bb4147ece472c9beb
# Parent  78688a5fafc28bc16d5a447208a4eb71d557cd9e
Thm.def_name;

diff -r 78688a5fafc2 -r 4693938e9c2a src/HOL/Import/hol4rews.ML
--- a/src/HOL/Import/hol4rews.ML	Thu Oct 23 15:28:08 2008 +0200
+++ b/src/HOL/Import/hol4rews.ML	Thu Oct 23 15:28:39 2008 +0200
@@ -617,7 +617,7 @@
 	  | NONE =>
 	    let
 		val used = HOL4UNames.get thy
-		val defname = def_name name
+		val defname = Thm.def_name name
 		val pdefname = name ^ "_primdef"
 	    in
 		if not (defname mem used)
diff -r 78688a5fafc2 -r 4693938e9c2a src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Thu Oct 23 15:28:08 2008 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Thu Oct 23 15:28:39 2008 +0200
@@ -1943,7 +1943,7 @@
         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
@@ -2038,7 +2038,7 @@
             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