src/HOL/Tools/res_atp.ML
changeset 26662 39483503705f
parent 26501 494f418cc51c
child 26675 fba93ce71435
--- 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)) =