src/HOL/Tools/refute.ML
changeset 36374 19c0c4b8b445
parent 36130 9a672f7d488d
child 36555 8ff45c2076da
     1.1 --- a/src/HOL/Tools/refute.ML	Fri Apr 23 16:55:51 2010 +0200
     1.2 +++ b/src/HOL/Tools/refute.ML	Fri Apr 23 16:59:48 2010 +0200
     1.3 @@ -1357,7 +1357,6 @@
     1.4      val subst_t = Term.subst_bounds (map Free frees, strip_t)
     1.5    in
     1.6      find_model thy (actual_params thy params) assm_ts subst_t true
     1.7 -    handle REFUTE (s, s') => error ("REFUTE " ^ s ^ " " ^ s') (* ### *)
     1.8    end;
     1.9  
    1.10  (* ------------------------------------------------------------------------- *)