src/HOL/Tools/typedef.ML

   let
     val args = map (apsnd (prep_constraint lthy)) raw_args;
     val ((goal, goal_pat, typedef_result), lthy') =
       prepare_typedef prep_term def name (b, args, mx) set opt_morphs lthy;
     fun after_qed [[th]] = snd o typedef_result th;
-  in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] lthy' end;
+  in Proof.theorem NONE after_qed [[(goal, [goal_pat])]] lthy' end;
 
 in
 
 val typedef = gen_typedef Syntax.check_term (K I);
 val typedef_cmd = gen_typedef Syntax.read_term Typedecl.read_constraint;