--- a/src/HOL/Decision_Procs/Cooper.thy Sat Mar 24 16:27:04 2012 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy Sun Mar 25 20:15:39 2012 +0200
@@ -1883,7 +1883,8 @@
| SOME n => @{code Bound} n)
| num_of_term vs @{term "0::int"} = @{code C} 0
| num_of_term vs @{term "1::int"} = @{code C} 1
- | num_of_term vs (@{term "number_of :: int \<Rightarrow> int"} $ t) = @{code C} (HOLogic.dest_numeral t)
+ | num_of_term vs (@{term "numeral :: _ \<Rightarrow> int"} $ t) = @{code C} (HOLogic.dest_num t)
+ | num_of_term vs (@{term "neg_numeral :: _ \<Rightarrow> int"} $ t) = @{code C} (~(HOLogic.dest_num t))
| num_of_term vs (Bound i) = @{code Bound} i
| num_of_term vs (@{term "uminus :: int \<Rightarrow> int"} $ t') = @{code Neg} (num_of_term vs t')
| num_of_term vs (@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =