# HG changeset patch
# User haftmann
# Date 1273161560 -7200
# Node ID 5f612b6d64a8053c3a354d58d93e51b5fe8f9af8
# Parent  ae84ddf03c58101b24a4083bc6dd626d7df8eab6
tuned

diff -r ae84ddf03c58 -r 5f612b6d64a8 src/HOL/Tools/Qelim/cooper_data.ML
--- a/src/HOL/Tools/Qelim/cooper_data.ML	Thu May 06 17:59:19 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper_data.ML	Thu May 06 17:59:20 2010 +0200
@@ -1,5 +1,4 @@
 (*  Title:      HOL/Tools/Qelim/cooper_data.ML
-    ID:         $Id$
     Author:     Amine Chaieb, TU Muenchen
 *)
 
@@ -16,8 +15,7 @@
 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 allowed_consts = 
   [@{term "op + :: int => _"}, @{term "op + :: nat => _"},
    @{term "op - :: int => _"}, @{term "op - :: nat => _"},
@@ -47,7 +45,7 @@
 structure Data = Generic_Data
 (
   type T = simpset * term list;
-  val empty = (start_ss, allowed_consts);
+  val empty = (HOL_ss, allowed_consts);
   val extend  = I;
   fun merge ((ss1, ts1), (ss2, ts2)) =
     (merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2));
@@ -64,7 +62,7 @@
      (ss delsimps [th], subtract (op aconv) ts' ts ))) 
 
 
-(* concrete syntax *)
+(* theory setup *)
 
 local
 
@@ -79,16 +77,11 @@
 
 in
 
-val presburger_setup =
+val setup =
   Attrib.setup @{binding presburger}
     ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
       optional (keyword constsN |-- terms) >> add) "Cooper data";
 
 end;
 
-
-(* theory setup *)
-
-val setup = presburger_setup;
-
 end;