removed obsolete PureThy.thms_containing;
authorwenzelm
Sat, 15 Mar 2008 18:08:54 +0100
changeset 26285 3905e52a1a0e
parent 26284 533dcb120a8e
child 26286 3ff5d257f175
removed obsolete PureThy.thms_containing;
src/Tools/code/code_package.ML
--- 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