src/Tools/code/code_package.ML
changeset 26690 e30b8d500c7d
parent 26662 39483503705f
child 26740 6c8cd101f875
--- 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