src/HOL/Tools/recdef.ML

     val i = the_default 1 opt_i;
     val tc = nth tcs (i - 1) handle Subscript =>
       error ("No termination condition #" ^ string_of_int i ^
         " in recdef definition of " ^ quote name);
   in
-    Specification.theorem Thm.internalK NONE (K I) (Binding.name bname, atts)
-      [] (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
+    Specification.theorem Thm.internalK NONE (K I)
+      (Binding.conceal (Binding.name bname), atts) []
+      (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
   end;
 
 val recdef_tc = gen_recdef_tc Attrib.intern_src Sign.intern_const;
 val recdef_tc_i = gen_recdef_tc (K I) (K I);