# HG changeset patch
# User wenzelm
# Date 1729542487 -7200
# Node ID b61abd1e502754f12799f5ea0e53001676bba7f2
# Parent  274344c65e018153fbad0ed3c6d8f53b4d2372ef
notable performance tuning (amending a59d9b81be24 and 8976c5bc9e97): avoid costly could_beta_eta_contract, which traverses the whole term;
always use Item_Net.retrieve instead, but on frozen TVars/Vars to enforce matching instead of unification;

diff -r 274344c65e01 -r b61abd1e5027 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Oct 21 20:02:27 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Oct 21 22:28:07 2024 +0200
@@ -666,19 +666,19 @@
     val thy = theory_of ctxt;
     val consts = consts_of ctxt;
     val Mode {abbrev, ...} = get_mode ctxt;
-
-    val nets = Consts.revert_abbrevs consts (print_mode_value () @ [""]);
-    fun match_abbrev t =
-      let
-        val retrieve =
-          if Term.could_beta_eta_contract t
-          then Item_Net.retrieve
-          else Item_Net.retrieve_matching;
-        fun match_rew net = get_first (Pattern.match_rew thy t) (retrieve net t);
-      in Option.map #1 (get_first match_rew nets) end;
   in
     if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of tm) then tm
-    else Pattern.rewrite_term_top thy [] [match_abbrev] tm
+    else
+      let
+        val inst = #1 (Variable.import_inst true [tm] ctxt);
+        val nets = Consts.revert_abbrevs consts (print_mode_value () @ [""]);
+        val rew = Option.map #1 oo Pattern.match_rew thy;
+        fun match_abbrev t = get_first (fn net => get_first (rew t) (Item_Net.retrieve net t)) nets;
+      in
+        Term_Subst.instantiate inst tm
+        |> Pattern.rewrite_term_top thy [] [match_abbrev]
+        |> Term_Subst.instantiate_frees (Variable.import_inst_revert inst)
+      end
   end;
 
 
diff -r 274344c65e01 -r b61abd1e5027 src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Oct 21 20:02:27 2024 +0200
+++ b/src/Pure/term.ML	Mon Oct 21 22:28:07 2024 +0200
@@ -183,7 +183,6 @@
   val maxidx_term: term -> int -> int
   val could_beta_contract: term -> bool
   val could_eta_contract: term -> bool
-  val could_beta_eta_contract: term -> bool
   val used_free: string -> term -> bool
   exception USED_FREE of string * term
   val dest_abs_fresh: string -> term -> (string * typ) * term
@@ -1045,12 +1044,6 @@
   | could_eta_contract (t $ u) = could_eta_contract t orelse could_eta_contract u
   | could_eta_contract _ = false;
 
-fun could_beta_eta_contract (Abs _ $ _) = true
-  | could_beta_eta_contract (Abs (_, _, _ $ Bound 0)) = true
-  | could_beta_eta_contract (Abs (_, _, b)) = could_beta_eta_contract b
-  | could_beta_eta_contract (t $ u) = could_beta_eta_contract t orelse could_beta_eta_contract u
-  | could_beta_eta_contract _ = false;
-
 
 (* dest abstraction *)
 
diff -r 274344c65e01 -r b61abd1e5027 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Mon Oct 21 20:02:27 2024 +0200
+++ b/src/Pure/variable.ML	Mon Oct 21 22:28:07 2024 +0200
@@ -72,6 +72,7 @@
   val importT_inst: term list -> Proof.context -> typ TVars.table * Proof.context
   val import_inst: bool -> term list -> Proof.context ->
     (typ TVars.table * term Vars.table) * Proof.context
+  val import_inst_revert: typ TVars.table * term Vars.table -> typ TFrees.table * term Frees.table
   val importT_terms: term list -> Proof.context -> term list * Proof.context
   val import_terms: bool -> term list -> Proof.context -> term list * Proof.context
   val importT: thm list -> Proof.context -> (ctyp TVars.table * thm list) * Proof.context
@@ -615,6 +616,15 @@
     val inst = Vars.build (fold2 (fn (x, T) => fn y => Vars.add ((x, T), Free (y, T))) vars ys);
   in ((instT, inst), ctxt'') end;
 
+fun import_inst_revert (instT, inst) =
+  let
+    val instT' = TFrees.build (instT |> TVars.fold (fn (v, TFree w) => TFrees.add (w, TVar v)));
+    val instantiateT' = Term_Subst.instantiateT_frees instT';
+    val inst' =
+      Frees.build (inst |> Vars.fold (fn ((xi, T), Free (y, U)) =>
+        Frees.add ((y, instantiateT' U), Var (xi, instantiateT' T))));
+  in (instT', inst') end;
+
 fun importT_terms ts ctxt =
   let val (instT, ctxt') = importT_inst ts ctxt
   in (map (Term_Subst.instantiate (instT, Vars.empty)) ts, ctxt') end;