diff -r 01ef1135de73 -r a7c128816edc src/HOL/Tools/Presburger/cooper_data.ML
--- a/src/HOL/Tools/Presburger/cooper_data.ML	Thu Jun 14 22:59:39 2007 +0200
+++ b/src/HOL/Tools/Presburger/cooper_data.ML	Thu Jun 14 22:59:40 2007 +0200
@@ -16,8 +16,8 @@
 struct
 
 type entry = simpset* (term list);
-val start_ss = HOL_ss addsimps @{thms "Groebner_Basis.comp_arith"}
-               addcongs [if_weak_cong, @{thm "let_weak_cong"}];
+val start_ss = HOL_ss (* addsimps @{thms "Groebner_Basis.comp_arith"}
+               addcongs [if_weak_cong, @{thm "let_weak_cong"}];*)
 val allowed_consts = 
   [@{term "op + :: int => _"}, @{term "op + :: nat => _"}, 
    @{term "op - :: int => _"}, @{term "op - :: nat => _"},