src/HOL/Tools/recdef.ML

--- a/src/HOL/Tools/recdef.ML	Thu Nov 12 21:59:35 2009 +0100
+++ b/src/HOL/Tools/recdef.ML	Thu Nov 12 22:02:11 2009 +0100
@@ -263,7 +263,7 @@
       error ("No termination condition #" ^ string_of_int i ^
         " in recdef definition of " ^ quote name);
   in
-    Specification.theorem Thm.internalK NONE (K I)
+    Specification.theorem "" NONE (K I)
       (Binding.conceal (Binding.name bname), atts) []
       (Element.Shows [(Attrib.empty_binding, [(HOLogic.mk_Trueprop tc, [])])]) int lthy
   end;