src/HOL/Decision_Procs/Cooper.thy
changeset 47108 2a1953f0d20d
parent 45740 132a3e1c0fe5
child 47142 d64fa2ca54b8
     1.1 --- a/src/HOL/Decision_Procs/Cooper.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Cooper.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -1883,7 +1883,8 @@
     1.4        | SOME n => @{code Bound} n)
     1.5    | num_of_term vs @{term "0::int"} = @{code C} 0
     1.6    | num_of_term vs @{term "1::int"} = @{code C} 1
     1.7 -  | num_of_term vs (@{term "number_of :: int \<Rightarrow> int"} $ t) = @{code C} (HOLogic.dest_numeral t)
     1.8 +  | num_of_term vs (@{term "numeral :: _ \<Rightarrow> int"} $ t) = @{code C} (HOLogic.dest_num t)
     1.9 +  | num_of_term vs (@{term "neg_numeral :: _ \<Rightarrow> int"} $ t) = @{code C} (~(HOLogic.dest_num t))
    1.10    | num_of_term vs (Bound i) = @{code Bound} i
    1.11    | num_of_term vs (@{term "uminus :: int \<Rightarrow> int"} $ t') = @{code Neg} (num_of_term vs t')
    1.12    | num_of_term vs (@{term "op + :: int \<Rightarrow> int \<Rightarrow> int"} $ t1 $ t2) =