diff --git a/books/doc/relnotes.lisp b/books/doc/relnotes.lisp
index 5a558d4ecbf..49b2f470b8d 100644
--- a/books/doc/relnotes.lisp
+++ b/books/doc/relnotes.lisp
@@ -117,6 +117,10 @@
  <p>Added a <see topic='@(url fty)'>fixtype</see>
  for <see topic='@(url set::std/osets)'>finite sets</see>.</p>
 
+ <p>Improved the @('copy-def') utility (community book
+ @('kestrel/utilities/copy-def.lisp')) by adding an @(':expand') hint in the
+ recursive case, as is sometimes necessary.</p>
+
  <h4><see topic='@(url soft::soft)'>SOFT</see></h4>
 
  <p>Added a @(':print') option to control screen output.</p>
diff --git a/books/kestrel/utilities/copy-def.lisp b/books/kestrel/utilities/copy-def.lisp
index b047e04460a..0324a4daa09 100644
--- a/books/kestrel/utilities/copy-def.lisp
+++ b/books/kestrel/utilities/copy-def.lisp
@@ -175,7 +175,8 @@
        ,@(and (eq flagp nil)
               `(:hints
                 (("Goal"
-                  ,@(and singly-recursivep `(:induct ,fn-call)))
+                  ,@(and singly-recursivep `(:induct ,fn-call))
+                  :expand (,fn-call ,fn-copy-call))
                  ,@(and hyps-preserved-thm-names
                         `('(:use (,@hyps-preserved-thm-names)))))))
        ,@(and (eq flagp t)