--- a/src/HOL/Tools/Qelim/cooper.ML Mon May 11 15:18:32 2009 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Mon May 11 15:57:29 2009 +0200
@@ -172,7 +172,7 @@
(* Canonical linear form for terms, formulae etc.. *)
fun provelin ctxt t = Goal.prove ctxt [] [] t
- (fn _ => EVERY [simp_tac lin_ss 1, TRY (linear_arith_tac ctxt 1)]);
+ (fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]);
fun linear_cmul 0 tm = zero
| linear_cmul n tm = case tm of
Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b