diff -r c79fa63504c8 -r b6e345548913 src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Tue May 03 15:37:41 2005 +0200
+++ b/src/HOL/arith_data.ML	Wed May 04 08:36:10 2005 +0200
@@ -173,7 +173,6 @@
 struct
 val ccontr = ccontr;
 val conjI = conjI;
-val neqE = linorder_neqE;
 val notI = notI;
 val sym = sym;
 val not_lessD = linorder_not_less RS iffD1;
@@ -418,12 +417,13 @@
 
 val init_lin_arith_data =
  Fast_Arith.setup @
- [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, simpset = _} =>
+ [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
    {add_mono_thms = add_mono_thms @
     add_mono_thms_ordered_semiring @ add_mono_thms_ordered_field,
     mult_mono_thms = mult_mono_thms,
     inj_thms = inj_thms,
     lessD = lessD @ [Suc_leI],
+    neqE = [linorder_neqE_nat],
     simpset = HOL_basic_ss addsimps add_rules
                    addsimprocs [ab_group_add_cancel.sum_conv, 
                                 ab_group_add_cancel.rel_conv]