diff -r c98a64746c69 -r dd5fe091ff04 src/HOL/Tools/int_factor_simprocs.ML
--- a/src/HOL/Tools/int_factor_simprocs.ML	Mon Mar 23 19:01:15 2009 +0100
+++ b/src/HOL/Tools/int_factor_simprocs.ML	Mon Mar 23 19:01:15 2009 +0100
@@ -232,7 +232,7 @@
       val less = Const(@{const_name HOL.less}, [T,T] ---> HOLogic.boolT);
       val pos = less $ zero $ t and neg = less $ t $ zero
       fun prove p =
-        Option.map Eq_True_elim (LinArith.lin_arith_simproc ss p)
+        Option.map Eq_True_elim (Lin_Arith.lin_arith_simproc ss p)
         handle THM _ => NONE
     in case prove pos of
          SOME th => SOME(th RS pos_th)