--- a/src/HOL/Tools/Presburger/cooper.ML Tue Jun 12 23:14:29 2007 +0200
+++ b/src/HOL/Tools/Presburger/cooper.ML Tue Jun 12 23:39:02 2007 +0200
@@ -25,7 +25,7 @@
val false_tm = @{cterm "False"};
val zdvd1_eq = @{thm "zdvd1_eq"};
val presburger_ss = @{simpset} addsimps [zdvd1_eq];
-val lin_ss = presburger_ss addsimps (@{thm "dvd_eq_mod_eq_0"}::zdvd1_eq::zadd_ac);
+val lin_ss = presburger_ss addsimps (@{thm "dvd_eq_mod_eq_0"}::zdvd1_eq::@{thms zadd_ac});
(* Some types and constants *)
val iT = HOLogic.intT
val bT = HOLogic.boolT;
@@ -658,4 +658,4 @@
(HOLogic.mk_Trueprop (term_of_qf ps vs (pa (qf_of_term ps vs t))))
end;
-end;
\ No newline at end of file
+end;