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