# HG changeset patch
# User haftmann
# Date 1273157879 -7200
# Node ID e6933119ea65c27f6d097b8a7546b4436fbf3315
# Parent  b6a47c7d6125476d43e6e63c358b080e3e85f4c8
fail on merge of conflicting normalization entries: functions are not mergable

diff -r b6a47c7d6125 -r e6933119ea65 src/HOL/Tools/Groebner_Basis/normalizer.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 16:57:28 2010 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 16:57:59 2010 +0200
@@ -55,7 +55,7 @@
   type T = (thm * entry) list;
   val empty = [];
   val extend = I;
-  val merge = AList.merge Thm.eq_thm (K true);
+  val merge = AList.merge Thm.eq_thm (K false);
 );
 
 val get = Data.get o Context.Proof;