src/HOL/Tools/typedef_package.ML

       cat_error msg ("Failed to prove non-emptiness of " ^ quote (string_of_term set));
   in typedef_result non_empty thy end;
 
 in
 
-val add_typedef = gen_typedef ProofContext.read_term;
-val add_typedef_i = gen_typedef ProofContext.cert_term;
+val add_typedef = gen_typedef Syntax.read_term;
+val add_typedef_i = gen_typedef Syntax.check_term;
 
 end;
 
 
 (* Isar typedef interface *)

     fun after_qed [[th]] = ProofContext.theory (snd o typedef_result th);
   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;
+val typedef = gen_typedef Syntax.read_term;
+val typedef_i = gen_typedef Syntax.check_term;
 
 end;