| changeset 28677 | 4693938e9c2a |
| parent 26928 | ca87aff1ad2d |
| child 28965 | 1de908189869 |
--- 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)