# HG changeset patch
# User wenzelm
# Date 1208278155 -7200
# Node ID 39483503705fea48804a7857e62c02aee6796044
# Parent  53e541e5b432bc7f61dd140e1ea3e50a4fd15067
Facts.dest_table;

diff -r 53e541e5b432 -r 39483503705f src/HOL/Import/shuffler.ML
--- 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
diff -r 53e541e5b432 -r 39483503705f src/HOL/Tools/res_atp.ML
--- 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)) =
diff -r 53e541e5b432 -r 39483503705f src/Tools/code/code_package.ML
--- 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