# HG changeset patch
# User haftmann
# Date 1241782701 -7200
# Node ID 796d3d42c87373cf3026ca077157887a1c1f400d
# Parent  845a6acd3bf363fb04b4572847e63e8a988b3ed3
proper structure name

diff -r 845a6acd3bf3 -r 796d3d42c873 src/HOL/Word/WordArith.thy
--- a/src/HOL/Word/WordArith.thy	Fri May 08 13:34:27 2009 +0200
+++ b/src/HOL/Word/WordArith.thy	Fri May 08 13:38:21 2009 +0200
@@ -701,7 +701,8 @@
   apply (erule (2) udvd_decr0)
   done
 
-ML{*Delsimprocs cancel_factors*}
+ML {* Delsimprocs Numeral_Simprocs.cancel_factors *}
+
 lemma udvd_incr2_K: 
   "p < a + s ==> a <= a + s ==> K udvd s ==> K udvd p - a ==> a <= p ==> 
     0 < K ==> p <= p + K & p + K <= a + s"
@@ -717,7 +718,8 @@
    apply arith
   apply simp
   done
-ML{*Delsimprocs cancel_factors*}
+
+ML {* Addsimprocs Numeral_Simprocs.cancel_factors *}
 
 (* links with rbl operations *)
 lemma word_succ_rbl: