1.1 --- a/src/HOL/Tools/meson.ML	Tue Dec 18 17:37:25 2007 +0100
     1.2 +++ b/src/HOL/Tools/meson.ML	Tue Dec 18 18:39:00 2007 +0100
     1.3 @@ -525,6 +525,13 @@
     1.4                     (tryres (th, [conj_forward, disj_forward, all_forward])))
     1.5      handle THM _ => forward_res skolemize (rename_bvs_RS th ex_forward);
     1.6  
     1.7 +fun skolemize_nnf_list [] = []
     1.8 +  | skolemize_nnf_list (th::ths) = 
     1.9 +      skolemize (make_nnf th) :: skolemize_nnf_list ths
    1.10 +      handle THM _ =>
    1.11 +       (warning ("Failed to Skolemize " ^ string_of_thm th);
    1.12 +        skolemize_nnf_list ths);
    1.13 +
    1.14  fun add_clauses (th,cls) =
    1.15    let val ctxt0 = Variable.thm_context th
    1.16        val (cnfs,ctxt) = make_cnf [] th ctxt0
    1.17 @@ -552,7 +559,7 @@
    1.18  fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
    1.19  
    1.20  fun skolemize_prems_tac prems =
    1.21 -    cut_facts_tac (map (skolemize o make_nnf) prems)  THEN'
    1.22 +    cut_facts_tac (skolemize_nnf_list prems) THEN'
    1.23      REPEAT o (etac exE);
    1.24  
    1.25  (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
    1.26 @@ -674,7 +681,7 @@
    1.27    let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
    1.28    in
    1.29       EVERY' [METAHYPS
    1.30 -            (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
    1.31 +            (fn hyps => (cut_facts_tac (skolemize_nnf_list hyps) 1
    1.32                           THEN REPEAT (etac exE 1))),
    1.33              REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
    1.34    end