src/HOL/Tools/typedef_package.ML

     val (cset, cset_pat, do_typedef) = prepare_typedef prep_term false name typ set thy;
     val goal = Thm.term_of (goal_nonempty true cset);
     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;
 
 val typedef_proof = gen_typedef_proof read_term;
 val typedef_proof_i = gen_typedef_proof cert_term;