# HG changeset patch
# User chaieb
# Date 1233747155 0
# Node ID 67266b31cd46a15180a70007e215c18b703f1bb8
# Parent  7c7f759c438ead74e8f3cae85eb9afe2260d9ac7# Parent  f73a68c9d810e1aa0cafb99242ec54010902c55f
merged

diff -r 7c7f759c438e -r 67266b31cd46 src/HOL/Tools/Groebner_Basis/groebner.ML
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Feb 04 10:59:32 2009 +0100
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Feb 04 11:32:35 2009 +0000
@@ -712,7 +712,7 @@
 
 fun refute tm =
  if tm aconvc false_tm then assume_Trueprop tm else
-  let
+ ((let
    val (nths0,eths0) = List.partition (is_neg o concl) (HOLogic.conj_elims (assume_Trueprop tm))
    val  nths = filter (is_eq o dest_arg o concl) nths0
    val eths = filter (is_eq o concl) eths0
@@ -767,7 +767,7 @@
                         (equal_elim (arg_cong_rule cTrp (eqF_intr th4))
                    (reflexive l |> mk_object_eq))
    end
-  end
+  end) handle ERROR _ => raise CTERM ("Gorbner-refute: unable to refute",[tm]))
 
 fun ring tm =
  let