# HG changeset patch
# User wenzelm
# Date 1723054015 -7200
# Node ID cdae621613daf6bed3d99093a210fada8552dce1
# Parent  294f3734411ceb108f88ea47c45eae666457d3c4
more robust: only type inference with its finish/fixate phase (on contrast to dc387e3999ec), e.g. avoid accidental "improvement" of type class operations (free vs. const);

diff -r 294f3734411c -r cdae621613da src/HOL/Tools/Metis/metis_reconstruct.ML
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Aug 07 16:28:32 2024 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Wed Aug 07 20:06:55 2024 +0200
@@ -58,8 +58,8 @@
     lits |> map (atp_literal_of_metis type_enc) |> mk_aconns AOr
 
 fun polish_hol_terms ctxt (lifted, old_skolems) =
-  map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems)
-  #> Syntax.check_terms (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
+  map (reveal_lam_lifted lifted #> reveal_old_skolem_terms old_skolems) #>
+  Type_Infer_Context.infer_types_finished (Proof_Context.set_mode Proof_Context.mode_pattern ctxt)
 
 fun hol_clause_of_metis ctxt type_enc sym_tab concealed =
   Metis_Thm.clause
diff -r 294f3734411c -r cdae621613da src/Pure/type_infer_context.ML
--- a/src/Pure/type_infer_context.ML	Wed Aug 07 16:28:32 2024 +0200
+++ b/src/Pure/type_infer_context.ML	Wed Aug 07 20:06:55 2024 +0200
@@ -11,6 +11,7 @@
   val prepare_positions: Proof.context -> term list -> term list * (Position.T * typ) list
   val prepare: Proof.context -> term list -> int * term list
   val infer_types: Proof.context -> term list -> term list
+  val infer_types_finished: Proof.context -> term list -> term list
 end;
 
 structure Type_Infer_Context: TYPE_INFER_CONTEXT =
@@ -304,4 +305,7 @@
     val (_, ts') = Type_Infer.finish ctxt tye ([], ts);
   in ts' end;
 
+fun infer_types_finished ctxt =
+  infer_types ctxt #> Proof_Context.standard_term_check_finish ctxt;
+
 end;