--- a/src/HOL/Tools/SMT/smtlib_proof.ML Wed Aug 07 20:07:50 2024 +0200
+++ b/src/HOL/Tools/SMT/smtlib_proof.ML Wed Aug 07 20:11:05 2024 +0200
@@ -97,9 +97,7 @@
val needs_inferT = equal Term.dummyT orf Term.is_TVar
val needs_infer = Term.exists_type (Term.exists_subtype needs_inferT)
- fun infer_types ctxt =
- singleton (Type_Infer_Context.infer_types ctxt) #>
- singleton (Proof_Context.standard_term_check_finish ctxt)
+ fun infer_types ctxt = singleton (Type_Infer_Context.infer_types_finished ctxt)
fun infer ctxt t = if needs_infer t then infer_types ctxt t else t
val (t, {ctxt = ctxt', extra = names, ...}: ((string * (string * typ)) list, 'b) context) =