diff -r 76ac4dbb0a22 -r d637611b41bd src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sat Sep 04 14:46:32 2021 +0200
+++ b/src/Pure/Isar/specification.ML	Sat Sep 04 18:21:58 2021 +0200
@@ -281,7 +281,7 @@
 
     val _ =
       Proof_Display.print_consts int (Position.thread_data ()) lthy5
-        (member (op =) (Term.add_frees lhs' [])) [(x, T)];
+        (Term_Subst.Frees.defined (Term_Subst.add_frees lhs' Term_Subst.Frees.empty)) [(x, T)];
   in ((lhs, (def_name, th')), lthy5) end;
 
 val definition' = gen_def check_spec_open (K I);