# 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);