src/HOL/Tools/recdef_package.ML

     val i = if_none opt_i 1;
     val tc = Library.nth_elem (i - 1, tcs) handle Library.LIST _ =>
       error ("No termination condition #" ^ string_of_int i ^
         " in recdef definition of " ^ quote name);
   in
-    thy |> IsarThy.theorem_i Drule.internalK None
+    thy |> IsarThy.theorem_i Drule.internalK (None, [])
       (((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))), Comment.none) int
   end;
 
 val recdef_tc = gen_recdef_tc Attrib.global_attribute Sign.intern_const;
 val recdef_tc_i = gen_recdef_tc (K I) (K I);