src/HOL/Tools/recdef_package.ML

     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) (Name.binding bname, atts)
-      [] (Element.Shows [((Name.no_binding, []), [(HOLogic.mk_Trueprop tc, [])])]) int lthy
+      [] (Element.Shows [(Attrib.no_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);