--- a/src/HOL/Tools/res_axioms.ML Thu Nov 30 14:17:22 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML Thu Nov 30 14:17:25 2006 +0100
@@ -485,7 +485,7 @@
(case skolem thy (name, Thm.transfer thy th) of
NONE => ([th],thy)
| SOME (thy',cls) =>
- let val cls = map Drule.local_standard cls
+ let val cls = map Goal.close_result cls
in
if null cls then warning ("skolem_cache: empty clause set for " ^ name)
else ();
@@ -506,7 +506,7 @@
"" => skolem_thm th (*no name, so can't cache*)
| s => case Symtab.lookup (!clause_cache) s of
NONE =>
- let val cls = map Drule.local_standard (skolem_thm th)
+ let val cls = map Goal.close_result (skolem_thm th)
in Output.debug "inserted into cache";
change clause_cache (Symtab.update (s, (th, cls))); cls
end