# HG changeset patch
# User desharna
# Date 1745478993 -7200
# Node ID c17936c7a5095a8c4ad2eb15908015b646561b8a
# Parent  4b13f46ff8ff4dee873b402fbe2b8d98780bbbe9# Parent  318526b74e6f88391f0ce19a7a95fec44ea3107c
merged

diff -r 4b13f46ff8ff -r c17936c7a509 src/HOL/Tools/Metis/metis_instantiations.ML
--- a/src/HOL/Tools/Metis/metis_instantiations.ML	Wed Apr 23 17:34:13 2025 +0200
+++ b/src/HOL/Tools/Metis/metis_instantiations.ML	Thu Apr 24 09:16:33 2025 +0200
@@ -9,7 +9,7 @@
   type inst
 
   type infer_params = {
-    ctxt : Proof.context,
+    infer_ctxt : Proof.context,
     type_enc : string,
     lam_trans : string,
     th_name : thm -> string option,
@@ -27,8 +27,8 @@
   val table_of_thm_inst : thm * inst -> cterm Vars.table
   val pretty_name_inst : Proof.context -> string * inst -> Pretty.T
   val string_of_name_inst : Proof.context -> string * inst -> string
-  val infer_thm_insts : infer_params -> (thm * inst) list option
-  val instantiate_call : infer_params -> thm -> unit
+  val infer_thm_insts : Proof.context -> infer_params -> (thm * inst) list option
+  val instantiate_call : Proof.context -> infer_params -> thm -> unit
 end;
 
 structure Metis_Instantiations : METIS_INSTANTIATIONS =
@@ -45,7 +45,7 @@
 
 (* Params needed for inference of variable instantiations *)
 type infer_params = {
-  ctxt : Proof.context,
+  infer_ctxt : Proof.context,
   type_enc : string,
   lam_trans : string,
   th_name : thm -> string option,
@@ -149,7 +149,7 @@
 (* Find the theorem corresponding to a Metis axiom if it has a name.
  * "Theorems" are Isabelle theorems given to the metis tactic.
  * "Axioms" are clauses given to the Metis prover. *)
-fun metis_axiom_to_thm {ctxt, th_name, th_cls_pairs, axioms, ...} (msubst, maxiom) =
+fun metis_axiom_to_thm ctxt {th_name, th_cls_pairs, axioms, ...} (msubst, maxiom) =
   let
     val axiom = lookth axioms maxiom
   in
@@ -161,7 +161,8 @@
 (* Build a table : term Vartab.table list Thmtab.table that maps a theorem to a
  * list of variable substitutions (theorems can be instantiated multiple times)
  * from Metis substitutions *)
-fun metis_substs_to_table {ctxt, type_enc, lifted, new_skolem, sym_tab, ...} th_of_vars th_msubsts =
+fun metis_substs_to_table ctxt {infer_ctxt, type_enc, lifted, new_skolem, sym_tab, ...}
+    th_of_vars th_msubsts =
   let
     val _ = trace_msg ctxt (K "AXIOM SUBSTITUTIONS")
     val type_enc = type_enc_of_string Strict type_enc
@@ -179,7 +180,7 @@
     (* Infer types and replace "_" terms/types with schematic variables *)
     val infer_types_pattern =
       singleton (Type_Infer_Context.infer_types_finished
-        (Proof_Context.set_mode Proof_Context.mode_pattern ctxt))
+        (Proof_Context.set_mode Proof_Context.mode_pattern infer_ctxt))
 
     (* "undefined" if allowed and not using new_skolem, "_" otherwise. *)
     val undefined_pattern =
@@ -192,11 +193,16 @@
     (* Instantiate schematic and free variables *)
     val inst_vars_frees = map_aterms
       (fn t as Free (x, T) =>
-        (* an unfixed/internal free variable is unknown/inaccessible to the user,
+        (* an undeclared/internal free variable is unknown/inaccessible to the user,
          * so we replace it with "_" *)
-        if not (Variable.is_fixed ctxt x) orelse Name.is_internal (Variable.revert_fixed ctxt x)
-        then Term.dummy_pattern T
-        else t
+        let
+          val x' = Variable.revert_fixed ctxt x
+        in
+          if not (Variable.is_declared ctxt x') orelse Name.is_internal x' then
+            Term.dummy_pattern T
+          else
+            t
+        end
       | Var (_, T) =>
         (* a schematic variable can be replaced with any term,
          * so we replace it with "undefined" *)
@@ -237,7 +243,7 @@
       let
         val _ = trace_msg ctxt (fn () => "Metis axiom: " ^ Metis_Thm.toString maxiom)
         val _ = trace_msg ctxt (fn () => "Metis substitution: " ^ Metis_Subst.toString msubst)
-        val _ = trace_msg ctxt (fn () => "Isabelle axiom: " ^ Thm.string_of_thm ctxt axiom)
+        val _ = trace_msg ctxt (fn () => "Isabelle axiom: " ^ Thm.string_of_thm infer_ctxt axiom)
         val _ = trace_msg ctxt (fn () => "Isabelle theorem: " ^
           Thm.string_of_thm ctxt th ^ " (" ^ name ^ ")")
 
@@ -255,7 +261,7 @@
           (* cf. find_var in Metis_Reconstruct.inst_inference *)
           |> Option.mapPartial (fn name => List.find (fn (a, _) => a = name) vars)
           (* cf. subst_translation in Metis_Reconstruct.inst_inference *)
-          |> Option.map (fn var => (var, hol_term_of_metis ctxt type_enc sym_tab mt))
+          |> Option.map (fn var => (var, hol_term_of_metis infer_ctxt type_enc sym_tab mt))
 
         (* Build the substitution table and instantiate the remaining schematic variables *)
         fun build_subst_table substs =
@@ -275,7 +281,7 @@
           trace_msg ctxt (fn () => cat_lines ("Raw Isabelle substitution:" ::
             (raw_substs |> map (fn (var, t) =>
               Term.string_of_vname var ^ " |-> " ^
-              Syntax.string_of_term ctxt t))))
+              Syntax.string_of_term infer_ctxt t))))
 
         val subst = raw_substs
           |> map (apsnd polish_term)
@@ -319,16 +325,16 @@
         (t', Sign.typ_unify thy (T, U) (tyenv, maxidx'))
       end
 
-    (* Instantiate type variables with a type unifier or a dummy type
+    (* Instantiate type variables with a type unifier and import remaining ones
      * (cf. Drule.infer_instantiate_types) *)
     fun inst_unifier (ts, tyenv) =
       let
         val instT =
           TVars.build (tyenv |> Vartab.fold (fn (xi, (S, T)) =>
             TVars.add ((xi, S), Envir.norm_type tyenv T)))
-        val dummy_tvars = Term.map_types (map_type_tvar (K Term.dummyT))
+        val ts' = map (Term_Subst.instantiate (instT, Vars.empty)) ts
       in
-        map (dummy_tvars o Term_Subst.instantiate (instT, Vars.empty)) ts
+        Variable.importT_terms ts' ctxt |> fst
       end
 
     (* Build variable instantiations from a substitution table and instantiate
@@ -351,7 +357,7 @@
     Thmtab.fold_rev (fn (th, substs) => fold (add_subst th) substs) th_substs_table []
   end
 
-fun really_infer_thm_insts (infer_params as {ctxt, th_name, th_cls_pairs, mth, ...}) =
+fun really_infer_thm_insts ctxt (infer_params as {th_name, th_cls_pairs, mth, ...}) =
   let
     (* Compute the theorem variables ordered as in of-instantiations.
      * import_export_thm is used to get the same variables as in axioms. *)
@@ -361,8 +367,8 @@
 
     val th_insts =
       infer_metis_axiom_substs mth
-      |> map_filter (metis_axiom_to_thm infer_params)
-      |> metis_substs_to_table infer_params th_of_vars
+      |> map_filter (metis_axiom_to_thm ctxt infer_params)
+      |> metis_substs_to_table ctxt infer_params th_of_vars
       |> table_to_thm_insts ctxt th_of_vars
 
     val _ = trace_msg ctxt (fn () => cat_lines ("THEOREM INSTANTIATIONS" ::
@@ -386,12 +392,12 @@
   end
 
 (* Infer variable instantiations *)
-fun infer_thm_insts (infer_params as {ctxt, ...}) =
-  \<^try>\<open>SOME (really_infer_thm_insts infer_params)
+fun infer_thm_insts ctxt infer_params =
+  \<^try>\<open>SOME (really_infer_thm_insts ctxt infer_params)
     catch exn => (trace_msg ctxt (fn () => Runtime.exn_message exn); NONE)\<close>
 
 (* Write suggested command with of-instantiations *)
-fun write_command {ctxt, type_enc, lam_trans, th_name, ...} st th_insts =
+fun write_command ctxt {type_enc, lam_trans, th_name, ...} st th_insts =
   let
     val _ = trace_msg ctxt (K "SUGGEST OF-INSTANTIATIONS")
     val apply_str = if Thm.nprems_of st = 0 then "by" else "apply"
@@ -408,9 +414,9 @@
   end
 
 (* Infer variable instantiations and suggest of-instantiations *)
-fun instantiate_call infer_params st =
-  infer_thm_insts infer_params
+fun instantiate_call ctxt infer_params st =
+  infer_thm_insts ctxt infer_params
   |> Option.mapPartial (Option.filter (not o thm_insts_trivial))
-  |> Option.app (write_command infer_params st)
+  |> Option.app (write_command ctxt infer_params st)
 
 end;
diff -r 4b13f46ff8ff -r c17936c7a509 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Wed Apr 23 17:34:13 2025 +0200
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Thu Apr 24 09:16:33 2025 +0200
@@ -211,7 +211,7 @@
             val _ =
               if exists is_some (map th_name used_ths) then
                 infer_params := SOME ({
-                  ctxt = ctxt',
+                  infer_ctxt = ctxt',
                   type_enc = type_enc_str,
                   lam_trans = lam_trans,
                   th_name = th_name,
@@ -308,7 +308,7 @@
     val instantiate_tac =
       if instantiate then
         (fn (NONE, st) => st
-          | (SOME infer_params, st) => tap (instantiate_call infer_params) st)
+          | (SOME infer_params, st) => tap (instantiate_call ctxt infer_params) st)
       else
         snd
   in
@@ -356,7 +356,7 @@
         (the_default default_metis_lam_trans lam_trans) false ctxt (schem_facts @ ths) i
   in
     Seq.THEN (insert_tac, metis_tac)
-    #> Seq.map (Option.mapPartial infer_thm_insts o fst)
+    #> Seq.map (Option.mapPartial (infer_thm_insts ctxt) o fst)
     #> Option.mapPartial fst o Seq.pull
   end