# HG changeset patch
# User blanchet
# Date 1643202336 -3600
# Node ID d2f97439f53e6de39bbcd3f0f1f469f0001a21b5
# Parent  43b3d5318d725ae7aad0206217f52fe44c3c7a6c
treat 'using X by meson' as 'by (meson X)' to avoid loss of polymorphism (cf. metis)

diff -r 43b3d5318d72 -r d2f97439f53e NEWS
--- a/NEWS	Tue Jan 25 14:13:33 2022 +0000
+++ b/NEWS	Wed Jan 26 14:05:36 2022 +0100
@@ -56,6 +56,9 @@
   - Added option "-y" for a dry run.
   - Renamed run_action to run in Mirabelle.action record. Minor INCOMPATIBILITY.
 
+* Meson
+  - Added support for polymorphic "using" facts. Minor INCOMPATIBILITY.
+
 
 
 *** System ***
diff -r 43b3d5318d72 -r d2f97439f53e src/HOL/Tools/Meson/meson_tactic.ML
--- a/src/HOL/Tools/Meson/meson_tactic.ML	Tue Jan 25 14:13:33 2022 +0000
+++ b/src/HOL/Tools/Meson/meson_tactic.ML	Wed Jan 26 14:05:36 2022 +0100
@@ -20,10 +20,20 @@
       false true 0) ths)
   end
 
+(* This is part of a workaround to avoid freezing schematic variables in \<^text>\<open>using\<close> facts. See
+   \<^file>\<open>~~/src/HOL/Tools/Metis/metis_tactic.ML\<close> for details. *)
+val has_tvar = exists_type (exists_subtype (fn TVar _ => true | _ => false)) o Thm.prop_of
+
 val _ =
   Theory.setup
-    (Method.setup \<^binding>\<open>meson\<close> (Attrib.thms >> (fn ths => fn ctxt =>
-      SIMPLE_METHOD' (CHANGED_PROP o meson_general_tac ctxt ths)))
+    (Method.setup \<^binding>\<open>meson\<close> (Attrib.thms >> (fn ths => fn ctxt0 =>
+      CONTEXT_METHOD (fn facts => fn (ctxt, st) =>
+        let val (schem_facts, nonschem_facts) = List.partition has_tvar facts in
+          st
+          |> HEADGOAL (Method.insert_tac ctxt nonschem_facts THEN'
+            CHANGED_PROP o meson_general_tac ctxt0 (schem_facts @ ths))
+          |> TACTIC_CONTEXT ctxt
+        end)))
       "MESON resolution proof procedure")
 
 end;