src/HOL/Tools/res_axioms.ML
changeset 22345 85f76b341893
parent 22218 30a8890d2967
child 22360 26ead7ed4f4b
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Wed Feb 21 13:51:12 2007 +0100
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Thu Feb 22 10:25:14 2007 +0100
     1.3 @@ -474,7 +474,7 @@
     1.4            let val (thy',defs) = declare_skofuns cname nnfth thy
     1.5                val cnfs = Meson.make_cnf (map skolem_of_def defs) nnfth
     1.6                val (thy'',cnfs') = declare_abstract (thy',cnfs)
     1.7 -          in (thy'', Meson.finish_cnf cnfs')
     1.8 +          in (map Goal.close_result (Meson.finish_cnf cnfs'), thy'')
     1.9            end)
    1.10        (SOME (to_nnf th)  handle THM _ => NONE)
    1.11    end;
    1.12 @@ -486,20 +486,17 @@
    1.13        NONE =>
    1.14          (case skolem thy (name, Thm.transfer thy th) of
    1.15               NONE => ([th],thy)
    1.16 -           | SOME (thy',cls) => 
    1.17 -               let val cls = map Goal.close_result cls
    1.18 -               in
    1.19 -                  if null cls then warning ("skolem_cache: empty clause set for " ^ name)
    1.20 +           | SOME (cls,thy') => 
    1.21 +                 (if null cls then warning ("skolem_cache: empty clause set for " ^ name)
    1.22                    else ();
    1.23                    change clause_cache (Symtab.update (name, (th, cls))); 
    1.24 -                  (cls,thy')
    1.25 -               end)
    1.26 +                  (cls,thy')))
    1.27      | SOME (th',cls) =>
    1.28          if eq_thm(th,th') then (cls,thy)
    1.29          else (Output.debug (fn () => "skolem_cache: Ignoring variant of theorem " ^ name);
    1.30                Output.debug (fn () => string_of_thm th);
    1.31                Output.debug (fn () => string_of_thm th');
    1.32 -              ([th],thy));
    1.33 +              getOpt (skolem thy (name, Thm.transfer thy th), ([th],thy)));
    1.34  
    1.35  (*Exported function to convert Isabelle theorems into axiom clauses*)
    1.36  fun cnf_axiom (name,th) =
    1.37 @@ -518,7 +515,7 @@
    1.38                      (Output.debug (fn () => "cnf_axiom: duplicate or variant of theorem " ^ name);
    1.39                       Output.debug (fn () => string_of_thm th);
    1.40                       Output.debug (fn () => string_of_thm th');
    1.41 -                     cls)
    1.42 +                     skolem_thm th)
    1.43   );
    1.44  
    1.45  fun pairname th = (PureThy.get_name_hint th, th);