Facts.dest_static;

--- a/src/HOL/Import/shuffler.ML	Wed Apr 16 20:43:31 2008 +0200
+++ b/src/HOL/Import/shuffler.ML	Wed Apr 16 21:52:58 2008 +0200
@@ -624,7 +624,7 @@
         val shuffles = ShuffleData.get thy
         val ignored = collect_ignored shuffles []
         val all_thms =
-          map (`PureThy.get_name_hint) (maps #2 (Facts.dest_table (PureThy.facts_of thy)))
+          map (`PureThy.get_name_hint) (maps #2 (Facts.dest_static (PureThy.facts_of thy)))
     in
         List.filter (match_consts ignored t) all_thms
     end

--- a/src/Pure/Isar/find_theorems.ML	Wed Apr 16 20:43:31 2008 +0200
+++ b/src/Pure/Isar/find_theorems.ML	Wed Apr 16 21:52:58 2008 +0200
@@ -273,8 +273,8 @@
 
 fun all_facts_of ctxt =
   maps Facts.selections
-   (Facts.dest_table (PureThy.facts_of (ProofContext.theory_of ctxt)) @
-    Facts.dest_table (ProofContext.facts_of ctxt));
+   (Facts.dest_static (PureThy.facts_of (ProofContext.theory_of ctxt)) @
+    Facts.dest_static (ProofContext.facts_of ctxt));
 
 val limit = ref 40;
 

--- a/src/Tools/code/code_package.ML	Wed Apr 16 20:43:31 2008 +0200
+++ b/src/Tools/code/code_package.ML	Wed Apr 16 21:52:58 2008 +0200
@@ -223,7 +223,7 @@
         val propdef = (((c, ty), tfree_vars @ map Free vars), t);
       in if c = "" then NONE else SOME (thmref, propdef) end;
   in
-    Facts.dest_table (PureThy.facts_of thy)
+    Facts.dest_static (PureThy.facts_of thy)
     |> maps Facts.selections
     |> map_filter select
     |> map_filter mk_codeprop