src/HOL/Tools/typedef_package.ML

--- a/src/HOL/Tools/typedef_package.ML	Mon Nov 13 10:34:32 2000 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Mon Nov 13 21:59:49 2000 +0100
@@ -239,7 +239,7 @@
     val goal_pat = Thm.term_of (goal_nonempty true cset_pat);
   in
     thy
-    |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef],
+    |> IsarThy.theorem_i ((("", [typedef_attribute cset do_typedef]),
       (goal, ([goal_pat], []))), comment) int
   end;