# HG changeset patch
# User paulson
# Date 1157388093 -7200
# Node ID 7ef72f030679caf6e84ebe14116f6a686089c053
# Parent  e993073eda4c26f468e684f17b09b5d9e7324a25
Using Drule.local_standard to reduce the space usage

diff -r e993073eda4c -r 7ef72f030679 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Mon Sep 04 17:06:45 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Mon Sep 04 18:41:33 2006 +0200
@@ -483,11 +483,14 @@
       NONE =>
         (case skolem thy (name, Thm.transfer thy th) of
              NONE => ([th],thy)
-           | SOME (thy',cls) =>
-               (if null cls then warning ("skolem_cache: empty clause set for " ^ name)
-                else ();
-                change clause_cache (Symtab.update (name, (th, map Drule.close_derivation cls)));
-                (cls,thy')))
+           | SOME (thy',cls) => 
+               let val cls = map Drule.local_standard cls
+               in
+                  if null cls then warning ("skolem_cache: empty clause set for " ^ name)
+                  else ();
+                  change clause_cache (Symtab.update (name, (th, cls))); 
+                  (cls,thy')
+               end)
     | SOME (th',cls) =>
         if eq_thm(th,th') then (cls,thy)
         else (Output.debug ("skolem_cache: Ignoring variant of theorem " ^ name);
@@ -500,8 +503,8 @@
   case name of
         "" => skolem_thm th (*no name, so can't cache*)
       | s  => case Symtab.lookup (!clause_cache) s of
-                NONE =>
-                  let val cls = skolem_thm th
+                NONE => 
+                  let val cls = map Drule.local_standard (skolem_thm th)
                   in change clause_cache (Symtab.update (s, (th, cls))); cls end
               | SOME(th',cls) =>
                   if eq_thm(th,th') then cls