1.1 --- a/src/HOL/Tools/meson.ML	Wed Dec 19 16:52:26 2007 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Wed Dec 19 17:40:48 2007 +0100
     1.3 @@ -528,7 +528,7 @@
     1.4  fun skolemize_nnf_list [] = []
     1.5    | skolemize_nnf_list (th::ths) = 
     1.6        skolemize (make_nnf th) :: skolemize_nnf_list ths
     1.7 -      handle THM _ =>
     1.8 +      handle THM _ => (*RS can fail if Unify.search_bound is too small*)
     1.9         (warning ("Failed to Skolemize " ^ string_of_thm th);
    1.10          skolemize_nnf_list ths);
    1.11