author | wenzelm |
Sat, 15 Mar 2008 18:08:54 +0100 | |
changeset 26285 | 3905e52a1a0e |
parent 26284 | 533dcb120a8e |
child 26286 | 3ff5d257f175 |
--- a/src/Tools/code/code_package.ML Sat Mar 15 18:08:04 2008 +0100 +++ b/src/Tools/code/code_package.ML Sat Mar 15 18:08:54 2008 +0100 @@ -194,7 +194,7 @@ val propdef = (((c, ty), tfree_vars @ map Free vars), t); in if c = "" then NONE else SOME (thmref, propdef) end; in - PureThy.thms_containing thy ([], []) + Facts.dest (PureThy.all_facts_of thy) |> maps PureThy.selections |> map_filter select |> map_filter mk_codeprop