src/HOL/Tools/typedef_package.ML

--- a/src/HOL/Tools/typedef_package.ML	Sun Nov 04 20:56:19 2001 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Sun Nov 04 20:56:59 2001 +0100
@@ -244,7 +244,7 @@
       prepare_typedef prep_term true name typ set opt_morphs thy;
     val att = #1 o att_result;
   in
-    thy |> IsarThy.theorem_i Drule.internalK None
+    thy |> IsarThy.theorem_i Drule.internalK (None, [])
       ((("", [att]), (goal, ([goal_pat], []))), comment) int
   end;