# HG changeset patch
# User paulson
# Date 1197999540 -3600
# Node ID cbb59ba6bf0c1f2cc70cd76d7e081c1eabfb6eac
# Parent  31232fe5a6add51427c9d89d3d5cf6f17d375924
Skolemization now catches exception THM, which may be raised if unification fails.

diff -r 31232fe5a6ad -r cbb59ba6bf0c src/HOL/Tools/meson.ML
--- a/src/HOL/Tools/meson.ML	Tue Dec 18 17:37:25 2007 +0100
+++ b/src/HOL/Tools/meson.ML	Tue Dec 18 18:39:00 2007 +0100
@@ -525,6 +525,13 @@
                    (tryres (th, [conj_forward, disj_forward, all_forward])))
     handle THM _ => forward_res skolemize (rename_bvs_RS th ex_forward);
 
+fun skolemize_nnf_list [] = []
+  | skolemize_nnf_list (th::ths) = 
+      skolemize (make_nnf th) :: skolemize_nnf_list ths
+      handle THM _ =>
+       (warning ("Failed to Skolemize " ^ string_of_thm th);
+        skolemize_nnf_list ths);
+
 fun add_clauses (th,cls) =
   let val ctxt0 = Variable.thm_context th
       val (cnfs,ctxt) = make_cnf [] th ctxt0
@@ -552,7 +559,7 @@
 fun gocls cls = name_thms "Goal#" (map make_goal (neg_clauses cls));
 
 fun skolemize_prems_tac prems =
-    cut_facts_tac (map (skolemize o make_nnf) prems)  THEN'
+    cut_facts_tac (skolemize_nnf_list prems) THEN'
     REPEAT o (etac exE);
 
 (*Basis of all meson-tactics.  Supplies cltac with clauses: HOL disjunctions.
@@ -674,7 +681,7 @@
   let val ts = Logic.strip_assums_hyp (List.nth (prems_of st, i-1))
   in
      EVERY' [METAHYPS
-            (fn hyps => (cut_facts_tac (map (skolemize o make_nnf) hyps) 1
+            (fn hyps => (cut_facts_tac (skolemize_nnf_list hyps) 1
                          THEN REPEAT (etac exE 1))),
             REPEAT_DETERM_N (length ts) o (etac thin_rl)] i st
   end