src/HOL/Tools/typedef_package.ML

 fun gen_typedef prep_term ((def, name), typ, set, opt_morphs) thy =
   let
     val (_, goal, goal_pat, typedef_result) =
       prepare_typedef prep_term def name typ set opt_morphs thy;
     fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th);
-  in
-    ProofContext.init thy
-    |> Proof.theorem_i PureThy.internalK NONE after_qed [[(goal, [goal_pat])]]
-  end;
+  in Proof.theorem_i NONE after_qed [[(goal, [goal_pat])]] (ProofContext.init thy) end;
 
 in
 
 val typedef = gen_typedef ProofContext.read_term;
 val typedef_i = gen_typedef ProofContext.cert_term;