# HG changeset patch
# User haftmann
# Date 1273167343 -7200
# Node ID 30cdc863a4f80b9b798f032b9b4441c489df403a
# Parent  2a72455be88bc6e8dc44cf25465e4c7b6b2d7755
revert to loose merge semantics

diff -r 2a72455be88b -r 30cdc863a4f8 src/HOL/Tools/Groebner_Basis/normalizer.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 19:27:51 2010 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 19:35:43 2010 +0200
@@ -55,7 +55,7 @@
   type T = (thm * entry) list;
   val empty = [];
   val extend = I;
-  val merge = AList.merge Thm.eq_thm (K false);
+  val merge = AList.merge Thm.eq_thm (K true);
 );
 
 val get = Data.get o Context.Proof;