# HG changeset patch
# User chaieb
# Date 1233747065 0
# Node ID f73a68c9d810e1aa0cafb99242ec54010902c55f
# Parent  c566b63ce76a5ef09f540bd5ecc5ca2f1c2238c4
Now catch ERROR exception thrown by find and friends

diff -r c566b63ce76a -r f73a68c9d810 src/HOL/Tools/Groebner_Basis/groebner.ML
--- a/src/HOL/Tools/Groebner_Basis/groebner.ML	Tue Feb 03 18:34:49 2009 +0100
+++ b/src/HOL/Tools/Groebner_Basis/groebner.ML	Wed Feb 04 11:31:05 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