diff -r b60f1fab408c -r 03ff4d1e6784 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/Tools/hologic.ML	Tue Nov 19 10:05:53 2013 +0100
@@ -104,7 +104,6 @@
   val mk_numeral: int -> term
   val dest_num: term -> int
   val numeral_const: typ -> term
-  val neg_numeral_const: typ -> term
   val add_numerals: term -> (term * typ) list -> (term * typ) list
   val mk_number: typ -> int -> term
   val dest_number: term -> typ * int
@@ -548,7 +547,6 @@
   | dest_num t = raise TERM ("dest_num", [t]);
 
 fun numeral_const T = Const ("Num.numeral_class.numeral", numT --> T);
-fun neg_numeral_const T = Const ("Num.neg_numeral_class.neg_numeral", numT --> T);
 
 fun add_numerals (Const ("Num.numeral_class.numeral", Type (_, [_, T])) $ t) = cons (t, T)
   | add_numerals (t $ u) = add_numerals t #> add_numerals u
@@ -559,14 +557,14 @@
   | mk_number T 1 = Const ("Groups.one_class.one", T)
   | mk_number T i =
     if i > 0 then numeral_const T $ mk_numeral i
-    else neg_numeral_const T $ mk_numeral (~ i);
+    else Const ("Groups.uminus_class.uminus", T --> T) $ mk_number T (~ i);
 
 fun dest_number (Const ("Groups.zero_class.zero", T)) = (T, 0)
   | dest_number (Const ("Groups.one_class.one", T)) = (T, 1)
   | dest_number (Const ("Num.numeral_class.numeral", Type ("fun", [_, T])) $ t) =
       (T, dest_num t)
-  | dest_number (Const ("Num.neg_numeral_class.neg_numeral", Type ("fun", [_, T])) $ t) =
-      (T, ~ (dest_num t))
+  | dest_number (Const ("Groups.uminus_class.uminus", Type ("fun", [_, T])) $ t) =
+      apsnd (op ~) (dest_number t)
   | dest_number t = raise TERM ("dest_number", [t]);