src/HOL/Tools/Qelim/cooper.ML
changeset 31101 26c7bb764a38
parent 30686 47a32dd1b86e
child 32264 0be31453f698
     1.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon May 11 15:18:32 2009 +0200
     1.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon May 11 15:57:29 2009 +0200
     1.3 @@ -172,7 +172,7 @@
     1.4  
     1.5      (* Canonical linear form for terms, formulae etc.. *)
     1.6  fun provelin ctxt t = Goal.prove ctxt [] [] t 
     1.7 -  (fn _ => EVERY [simp_tac lin_ss 1, TRY (linear_arith_tac ctxt 1)]);
     1.8 +  (fn _ => EVERY [simp_tac lin_ss 1, TRY (Lin_Arith.tac ctxt 1)]);
     1.9  fun linear_cmul 0 tm = zero 
    1.10    | linear_cmul n tm = case tm of  
    1.11        Const (@{const_name HOL.plus}, _) $ a $ b => addC $ linear_cmul n a $ linear_cmul n b