src/HOL/Tools/Qelim/cooper.ML

--- a/src/HOL/Tools/Qelim/cooper.ML	Mon Jul 30 19:46:15 2007 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Tue Jul 31 00:56:26 2007 +0200
@@ -173,7 +173,7 @@
 
     (* Canonical linear form for terms, formulae etc.. *)
 fun provelin ctxt t = Goal.prove ctxt [] [] t 
-                          (fn _ => EVERY [simp_tac lin_ss 1, TRY (simple_arith_tac 1)]);
+  (fn _ => EVERY [simp_tac lin_ss 1, TRY (simple_arith_tac ctxt 1)]);
 fun linear_cmul 0 tm =  zero 
   | linear_cmul n tm = 
     case tm of