src/HOL/Tools/Groebner_Basis/groebner.ML

 fun neq_rule n th = [prove_nz n, th] MRS neq_thm;
 fun mk_add th1 = combination(arg_cong_rule ring_add_tm th1);
 
 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
   in
    if null eths then

     val (l,r) = dest_eq(dest_arg(concl th4))
    in implies_intr (mk_comb cTrp tm)
                         (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
   fun mk_forall x p =
       mk_comb (cterm_rule (instantiate' [SOME (ctyp_of_term x)] []) @{cpat "All:: (?'a => bool) => _"}) (cabs x p)