Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more robust, notably for Isabelle/MAWEN "polyminus.sml matchsub (?a * (?b - ?c)..."; default tip
authorwenzelm
Wed, 13 Aug 2025 19:40:09 +0200
changeset 83005 a2a860cd3215
parent 83004 304519f22c2c
more robust, notably for Isabelle/MAWEN "polyminus.sml matchsub (?a * (?b - ?c)...";
src/Pure/Isar/proof_context.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle