src/HOL/Tools/recdef_package.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_i Thm.internalK NONE (K I) (bname, atts)
+    Specification.theorem Thm.internalK NONE (K I) (bname, atts)
       [] (Element.Shows [(("", []), [(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);