Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Thm.def_name;
authorwenzelm
Thu, 23 Oct 2008 15:28:39 +0200
changeset 28677 4693938e9c2a
parent 28676 78688a5fafc2
child 28678 d93980a6c3cb
Thm.def_name;
src/HOL/Import/hol4rews.ML file | annotate | diff | comparison | revisions
src/HOL/Import/proof_kernel.ML file | annotate | diff | comparison | revisions 
--- 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)
--- 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
isabelle