# HG changeset patch
# User desharna
# Date 1643269944 -3600
# Node ID 16f83cea1e0aec09e2496dd4f5ae42c932a0c510
# Parent  4261983ca0cef3a55249f23c4180bc5358d9b2c6# Parent  d2f97439f53e6de39bbcd3f0f1f469f0001a21b5
merged

diff -r 4261983ca0ce -r 16f83cea1e0a NEWS
--- a/NEWS	Wed Jan 26 16:49:56 2022 +0100
+++ b/NEWS	Thu Jan 27 08:52:24 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 4261983ca0ce -r 16f83cea1e0a src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Wed Jan 26 16:49:56 2022 +0100
+++ b/src/HOL/Library/More_List.thy	Thu Jan 27 08:52:24 2022 +0100
@@ -91,11 +91,11 @@
 where
   "no_leading P xs \<longleftrightarrow> (xs \<noteq> [] \<longrightarrow> \<not> P (hd xs))"
 
-lemma no_leading_Nil [simp, intro!]:
+lemma no_leading_Nil [iff]:
   "no_leading P []"
   by (simp add: no_leading_def)
 
-lemma no_leading_Cons [simp, intro!]:
+lemma no_leading_Cons [iff]:
   "no_leading P (x # xs) \<longleftrightarrow> \<not> P x"
   by (simp add: no_leading_def)
 
@@ -148,7 +148,7 @@
   "no_trailing P xs \<longleftrightarrow> (xs \<noteq> [] \<longrightarrow> \<not> P (last xs))"
   by (induct xs) simp_all
 
-lemma no_trailing_Nil [simp, intro!]:
+lemma no_trailing_Nil [iff]:
   "no_trailing P []"
   by simp
 
diff -r 4261983ca0ce -r 16f83cea1e0a src/HOL/Tools/Meson/meson_tactic.ML
--- a/src/HOL/Tools/Meson/meson_tactic.ML	Wed Jan 26 16:49:56 2022 +0100
+++ b/src/HOL/Tools/Meson/meson_tactic.ML	Thu Jan 27 08:52:24 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;