# HG changeset patch
# User wenzelm
# Date 1723380356 -7200
# Node ID e451d6230535732c828bd66f0c0355925b8403f1
# Parent  f65b65814b81c44525afe4a1696698f50704e9a2
tuned: more antiquotations;

diff -r f65b65814b81 -r e451d6230535 src/HOL/Tools/Qelim/qelim.ML
--- a/src/HOL/Tools/Qelim/qelim.ML	Sun Aug 11 14:18:40 2024 +0200
+++ b/src/HOL/Tools/Qelim/qelim.ML	Sun Aug 11 14:45:56 2024 +0200
@@ -16,20 +16,16 @@
 structure Qelim: QELIM =
 struct
 
-val all_not_ex = mk_meta_eq @{thm "all_not_ex"};
-
 fun gen_qelim_conv ctxt precv postcv simpex_conv ins env atcv ncv qcv =
   let
     fun conv env p =
-      case Thm.term_of p of
-        Const(s,T)$_$_ =>
-           if domain_type T = HOLogic.boolT
-              andalso member (op =) [\<^const_name>\<open>HOL.conj\<close>, \<^const_name>\<open>HOL.disj\<close>,
-                \<^const_name>\<open>HOL.implies\<close>, \<^const_name>\<open>HOL.eq\<close>] s
-           then Conv.binop_conv (conv env) p
-           else atcv env p
-      | Const(\<^const_name>\<open>Not\<close>,_)$_ => Conv.arg_conv (conv env) p
-      | Const(\<^const_name>\<open>Ex\<close>,_)$Abs (s, _, _) =>
+      (case Thm.term_of p of
+        \<^Const_>\<open>conj for _ _\<close> => Conv.binop_conv (conv env) p
+      | \<^Const_>\<open>disj for _ _\<close> => Conv.binop_conv (conv env) p
+      | \<^Const_>\<open>implies for _ _\<close> => Conv.binop_conv (conv env) p
+      | \<^Const_>\<open>HOL.eq _ for _ _\<close> => Conv.binop_conv (conv env) p
+      | \<^Const_>\<open>Not for _\<close> => Conv.arg_conv (conv env) p
+      | \<^Const_>\<open>Ex _ for \<open>Abs (s, _, _)\<close>\<close> =>
           let
             val (e,p0) = Thm.dest_comb p
             val (x,p') = Thm.dest_abs_global p0
@@ -43,15 +39,15 @@
             if Thm.is_reflexive th' then Thm.transitive th (qcv env (Thm.rhs_of th))
             else Thm.transitive (Thm.transitive th th') (conv env r)
           end
-      | Const(\<^const_name>\<open>Ex\<close>,_)$ _ => (Thm.eta_long_conversion then_conv conv env) p
-      | Const(\<^const_name>\<open>All\<close>, _)$_ =>
+      | \<^Const_>\<open>Ex _ for _\<close> => (Thm.eta_long_conversion then_conv conv env) p
+      | \<^Const_>\<open>All _ for _\<close> =>
           let
             val allT = Thm.ctyp_of_cterm (Thm.dest_fun p)
             val T = Thm.dest_ctyp0 (Thm.dest_ctyp0 allT)
-            val p = Thm.dest_arg p
-            val th = Thm.instantiate' [SOME T] [SOME p] all_not_ex
+            val P = Thm.dest_arg p
+            val th = \<^instantiate>\<open>'a = T and P in lemma "\<forall>x::'a. P x \<equiv> \<nexists>x. \<not> P x" by simp\<close>
           in Thm.transitive th (conv env (Thm.rhs_of th)) end
-      | _ => atcv env p
+      | _ => atcv env p)
   in precv then_conv (conv env) then_conv postcv end