changeset 30685 | dd5fe091ff04 |
parent 30649 | 57753e0ec1d4 |
child 30931 | 86ca651da03e |
--- 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)