# HG changeset patch
# User wenzelm
# Date 1635444246 -7200
# Node ID cce64b47d13af84cc7a206b96c721ab284c9a5a2
# Parent  7f6178b655a80f20b7f96d00dde0f556985ee1b5
clarified antiquotations;

diff -r 7f6178b655a8 -r cce64b47d13a src/HOL/Library/Sum_of_Squares/positivstellensatz.ML
--- a/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML	Thu Oct 28 20:01:59 2021 +0200
+++ b/src/HOL/Library/Sum_of_Squares/positivstellensatz.ML	Thu Oct 28 20:04:06 2021 +0200
@@ -177,6 +177,10 @@
      "((\<not>(x \<le> y)) \<equiv> (x - y > 0))" and "((\<not>(x = y)) \<equiv> (x - y > 0 \<or> -(x - y) > 0))"
   by (atomize (full), auto simp add: less_diff_eq le_diff_eq not_less)};
 
+fun neq_th x y =
+  \<^instantiate>\<open>x and y in lemma \<open>x \<noteq> y \<equiv> x - y > 0 \<or> - (x - y) > 0\<close> for x y :: real
+    by (atomize (full), auto simp add: less_diff_eq le_diff_eq not_less)\<close>;
+
 val pth_final = @{lemma "(\<not>p \<Longrightarrow> False) \<Longrightarrow> p" by blast}
 val pth_add =
   @{lemma "(x = (0::real) \<Longrightarrow> y = 0 \<Longrightarrow> x + y = 0 )" and "( x = 0 \<Longrightarrow> y \<ge> 0 \<Longrightarrow> x + y \<ge> 0)" and
@@ -475,11 +479,10 @@
         if is_binop b ct then Thm.dest_binop ct
         else raise CTERM ("dest_binary",[b,ct])
     val dest_eq = dest_binary \<^cterm>\<open>(=) :: real \<Rightarrow> _\<close>
-    val neq_th = nth pth 5
     fun real_not_eq_conv ct =
       let
         val (l,r) = dest_eq (Thm.dest_arg ct)
-        val th = Thm.instantiate (TVars.empty, Vars.make [(\<^var>\<open>?x::real\<close>,l),(\<^var>\<open>?y::real\<close>,r)]) neq_th
+        val th = neq_th l r
         val th_p = poly_conv(Thm.dest_arg(Thm.dest_arg1(Thm.rhs_of th)))
         val th_x = Drule.arg_cong_rule \<^cterm>\<open>uminus :: real \<Rightarrow> _\<close> th_p
         val th_n = fconv_rule (arg_conv poly_neg_conv) th_x