# HG changeset patch
# User wenzelm
# Date 1755106809 -7200
# Node ID a2a860cd32152484e5ac35e15cef467d1c56d077
# Parent  304519f22c2ce13b646ae8e2864ae808482f1f35
more robust, notably for Isabelle/MAWEN "polyminus.sml matchsub (?a * (?b - ?c)...";

diff -r 304519f22c2c -r a2a860cd3215 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Wed Aug 13 09:34:57 2025 +0200
+++ b/src/Pure/Isar/proof_context.ML	Wed Aug 13 19:40:09 2025 +0200
@@ -734,7 +734,7 @@
     if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of tm) then tm
     else
       let
-        val inst = #1 (Variable.import_inst true [tm] ctxt);
+        val inst = #1 (Variable.import_inst true [tm] (Variable.declare_names 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;