# HG changeset patch
# User haftmann
# Date 1178827895 -7200
# Node ID 0b53bd36258b908ab1ab22cf26175809b79caa9e
# Parent  fb6917e426dab9994685f8d98f86262a1b4a465c
fixed typo

diff -r fb6917e426da -r 0b53bd36258b src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Thu May 10 18:10:32 2007 +0200
+++ b/src/HOL/arith_data.ML	Thu May 10 22:11:35 2007 +0200
@@ -744,7 +744,7 @@
         val iszero_t2               = Const ("IntDef.iszero", split_type --> HOLogic.boolT) $ t2
         val neg_minus_k             = Const ("IntDef.neg", split_type --> HOLogic.boolT) $
                                         (number_of $
-                                          (Const ("Numeral.uminus",
+                                          (Const ("HOL.uminus",
                                             HOLogic.intT --> HOLogic.intT) $ k'))
         val zero_leq_j              = Const ("Orderings.less_eq",
                                         split_type --> split_type --> HOLogic.boolT) $ zero $ j