# HG changeset patch
# User paulson
# Date 1172136314 -3600
# Node ID 85f76b3418939ca9f7ac0d6da7b44f88171d96b1
# Parent  eddeabf16b5d3bf9f32bcf4eb4e0eec4fa9db6bc
Improved handling of situation when theorem in cache disagrees with theorem supplied: new clauses
are now returned, fixing a bug in the metis method.

diff -r eddeabf16b5d -r 85f76b341893 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Wed Feb 21 13:51:12 2007 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Thu Feb 22 10:25:14 2007 +0100
@@ -474,7 +474,7 @@
           let val (thy',defs) = declare_skofuns cname nnfth thy
               val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
               val (thy'',cnfs') = declare_abstract (thy',cnfs)
-          in (thy'', Meson.finish_cnf cnfs')
+          in (map Goal.close_result (Meson.finish_cnf cnfs'), thy'')
           end)
       (SOME (to_nnf th)  handle THM _ => NONE)
   end;
@@ -486,20 +486,17 @@
       NONE =>
         (case skolem thy (name, Thm.transfer thy th) of
              NONE => ([th],thy)
-           | SOME (thy',cls) => 
-               let val cls = map Goal.close_result cls
-               in
-                  if null cls then warning ("skolem_cache: empty clause set for " ^ name)
+           | SOME (cls,thy') => 
+                 (if null cls then warning ("skolem_cache: empty clause set for " ^ name)
                   else ();
                   change clause_cache (Symtab.update (name, (th, cls))); 
-                  (cls,thy')
-               end)
+                  (cls,thy')))
     | SOME (th',cls) =>
         if eq_thm(th,th') then (cls,thy)
         else (Output.debug (fn () => "skolem_cache: Ignoring variant of theorem " ^ name);
               Output.debug (fn () => string_of_thm th);
               Output.debug (fn () => string_of_thm th');
-              ([th],thy));
+              getOpt (skolem thy (name, Thm.transfer thy th), ([th],thy)));
 
 (*Exported function to convert Isabelle theorems into axiom clauses*)
 fun cnf_axiom (name,th) =
@@ -518,7 +515,7 @@
                     (Output.debug (fn () => "cnf_axiom: duplicate or variant of theorem " ^ name);
                      Output.debug (fn () => string_of_thm th);
                      Output.debug (fn () => string_of_thm th');
-                     cls)
+                     skolem_thm th)
  );
 
 fun pairname th = (PureThy.get_name_hint th, th);