src/HOL/Tools/refute.ML

--- a/src/HOL/Tools/refute.ML	Fri Apr 23 16:55:51 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Fri Apr 23 16:59:48 2010 +0200
@@ -1357,7 +1357,6 @@
     val subst_t = Term.subst_bounds (map Free frees, strip_t)
   in
     find_model thy (actual_params thy params) assm_ts subst_t true
-    handle REFUTE (s, s') => error ("REFUTE " ^ s ^ " " ^ s') (* ### *)
   end;
 
 (* ------------------------------------------------------------------------- *)