src/HOL/Tools/Qelim/cooper.ML

 	      in K (inst' [d,s] mindvd, FWD (inst' [d,s] bsetndvd) [dd], FWD (inst' [d,s] infDndvd) [dd]) end)
 | _ => ([], K (inst' [cp] miP, inst' [cp] bsetP, inst' [cp] infDP))
 
     (* 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 ctxt 1)]);
+  (fn _ => EVERY [simp_tac lin_ss 1, TRY (linear_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
     | Const (@{const_name HOL.times}, _) $ c $ x => mulC $ numeral1 (fn m => n * m) c $ x
     | Const (@{const_name HOL.minus}, _) $ a $ b => subC $ linear_cmul n a $ linear_cmul n b