src/HOL/Tools/typedef_package.ML

--- a/src/HOL/Tools/typedef_package.ML	Thu Jul 08 18:35:44 1999 +0200
+++ b/src/HOL/Tools/typedef_package.ML	Thu Jul 08 18:36:09 1999 +0200
@@ -195,7 +195,7 @@
     val goal = Thm.term_of (goal_nonempty cset);
   in
     thy
-    |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], (goal, [])), comment) int
+    |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], (goal, ([], []))), comment) int
   end;
 
 val typedef_proof = gen_typedef_proof read_term;