Facts.dest_table;

--- a/src/HOL/Import/shuffler.ML	Tue Apr 15 18:49:13 2008 +0200
+++ b/src/HOL/Import/shuffler.ML	Tue Apr 15 18:49:15 2008 +0200
@@ -623,7 +623,8 @@
     let
         val shuffles = ShuffleData.get thy
         val ignored = collect_ignored shuffles []
-        val all_thms = map (`PureThy.get_name_hint) (maps #2 (Facts.dest (PureThy.all_facts_of thy)))
+        val all_thms =
+          map (`PureThy.get_name_hint) (maps #2 (Facts.dest_table (PureThy.facts_of thy)))
     in
         List.filter (match_consts ignored t) all_thms
     end

--- a/src/HOL/Tools/res_atp.ML	Tue Apr 15 18:49:13 2008 +0200
+++ b/src/HOL/Tools/res_atp.ML	Tue Apr 15 18:49:15 2008 +0200
@@ -480,7 +480,7 @@
     fun dest_valid (space, tab) = Symtab.fold (extern_valid space) tab [];
   in
     maps (dest_valid o PureThy.theorems_of) all_thys @
-    fold (extern_valid (Facts.space_of local_facts)) (Facts.dest local_facts) []
+    fold (extern_valid (Facts.space_of local_facts)) (Facts.dest_table local_facts) []
   end;
 
 fun multi_name a (th, (n,pairs)) =

--- a/src/Tools/code/code_package.ML	Tue Apr 15 18:49:13 2008 +0200
+++ b/src/Tools/code/code_package.ML	Tue Apr 15 18:49:15 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 (PureThy.all_facts_of thy)
+    Facts.dest_table (PureThy.facts_of thy)
     |> maps Facts.selections
     |> map_filter select
     |> map_filter mk_codeprop