# HG changeset patch
# User wenzelm
# Date 1633167519 -7200
# Node ID ed4149b3d7ab835ea8d1cdfefe27bb96fcd93457
# Parent  baa7a208d9d55db29f6d30c89c2ca8d59220ca38
proper patterns for (- numeral t), amending 03ff4d1e6784;

diff -r baa7a208d9d5 -r ed4149b3d7ab src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Sat Oct 02 11:20:12 2021 +0200
+++ b/src/HOL/Decision_Procs/Cooper.thy	Sat Oct 02 11:38:39 2021 +0200
@@ -2388,7 +2388,7 @@
   | num_of_term vs \<^term>\<open>- 1::int\<close> = @{code C} (@{code int_of_integer} (~ 1))
   | num_of_term vs \<^Const_>\<open>numeral _ for t\<close> =
       @{code C} (@{code int_of_integer} (HOLogic.dest_numeral t))
-  | num_of_term vs (\<^term>\<open>- numeral :: _ \<Rightarrow> int\<close> $ t) =  (* FIXME !? *)
+  | num_of_term vs \<^Const_>\<open>uminus \<^Type>\<open>int\<close> for \<^Const_>\<open>numeral \<^Type>\<open>int\<close> for t\<close>\<close> =
       @{code C} (@{code int_of_integer} (~(HOLogic.dest_numeral t)))
   | num_of_term vs (Bound i) = @{code Bound} (@{code nat_of_integer} i)
   | num_of_term vs \<^Const_>\<open>uminus \<^Type>\<open>int\<close> for t'\<close> = @{code Neg} (num_of_term vs t')
diff -r baa7a208d9d5 -r ed4149b3d7ab src/HOL/Decision_Procs/MIR.thy
--- a/src/HOL/Decision_Procs/MIR.thy	Sat Oct 02 11:20:12 2021 +0200
+++ b/src/HOL/Decision_Procs/MIR.thy	Sat Oct 02 11:38:39 2021 +0200
@@ -5592,7 +5592,7 @@
       | _ => error "num_of_term: unsupported Multiplication")
   | num_of_term vs \<^Const_>\<open>of_int \<^Type>\<open>real\<close> for \<^Const_>\<open>numeral \<^Type>\<open>int\<close> for t'\<close>\<close> =
       mk_C (HOLogic.dest_numeral t')
-  | num_of_term vs (\<^Const_>\<open>of_int \<^Type>\<open>real\<close>\<close> $ (\<^term>\<open>- numeral :: _ \<Rightarrow> int\<close> $ t')) =  (* FIXME !? *)
+  | num_of_term vs \<^Const_>\<open>of_int \<^Type>\<open>real\<close> for \<^Const_>\<open>uminus \<^Type>\<open>int\<close> for \<^Const_>\<open>numeral \<^Type>\<open>int\<close> for t'\<close>\<close>\<close> =
       mk_C (~ (HOLogic.dest_numeral t'))
   | num_of_term vs \<^Const_>\<open>of_int \<^Type>\<open>real\<close> for \<^Const_>\<open>floor \<^Type>\<open>real\<close> for t'\<close>\<close> =
       @{code Floor} (num_of_term vs t')
@@ -5600,7 +5600,7 @@
       @{code Neg} (@{code Floor} (@{code Neg} (num_of_term vs t')))
   | num_of_term vs \<^Const_>\<open>numeral \<^Type>\<open>real\<close> for t'\<close> =
       mk_C (HOLogic.dest_numeral t')
-  | num_of_term vs (\<^term>\<open>- numeral :: _ \<Rightarrow> real\<close> $ t') =  (* FIXME !? *)
+  | num_of_term vs \<^Const_>\<open>uminus \<^Type>\<open>real\<close> for \<^Const_>\<open>numeral \<^Type>\<open>real\<close> for t'\<close>\<close> =
       mk_C (~ (HOLogic.dest_numeral t'))
   | num_of_term vs t = error ("num_of_term: unknown term " ^ Syntax.string_of_term \<^context> t);
 
@@ -5614,7 +5614,7 @@
       @{code Eq} (@{code Sub} (num_of_term vs t1, num_of_term vs t2))
   | fm_of_term vs \<^Const_>\<open>rdvd for \<^Const_>\<open>of_int \<^Type>\<open>real\<close> for \<^Const_>\<open>numeral \<^Type>\<open>int\<close> for t1\<close>\<close> t2\<close> =
       mk_Dvd (HOLogic.dest_numeral t1, num_of_term vs t2)
-  | fm_of_term vs \<^Const_>\<open>rdvd for \<^Const_>\<open>of_int \<^Type>\<open>real\<close> for \<open>(\<^term>\<open>- numeral :: _ \<Rightarrow> int\<close> $ t1)\<close>\<close> t2\<close> =  (* FIXME !? *)
+  | fm_of_term vs \<^Const_>\<open>rdvd for \<^Const_>\<open>of_int \<^Type>\<open>real\<close> for \<^Const_>\<open>uminus \<^Type>\<open>int\<close> for \<^Const_>\<open>numeral \<^Type>\<open>int\<close> for t1\<close>\<close>\<close> t2\<close> =
       mk_Dvd (~ (HOLogic.dest_numeral t1), num_of_term vs t2)
   | fm_of_term vs \<^Const_>\<open>HOL.eq \<^Type>\<open>bool\<close> for t1 t2\<close> =
       @{code Iff} (fm_of_term vs t1, fm_of_term vs t2)