diff -r c09427e5f554 -r 1703de633aaf src/HOL/Tools/recdef_package.ML
--- a/src/HOL/Tools/recdef_package.ML	Wed Oct 31 21:58:04 2001 +0100
+++ b/src/HOL/Tools/recdef_package.ML	Wed Oct 31 21:59:07 2001 +0100
@@ -310,7 +310,7 @@
       error ("No termination condition #" ^ string_of_int i ^
         " in recdef definition of " ^ quote name);
   in
-    thy |> IsarThy.theorem_i Drule.internalK
+    thy |> IsarThy.theorem_i Drule.internalK None
       (((bname, atts), (HOLogic.mk_Trueprop tc, ([], []))), Comment.none) int
   end;