Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed obsolete PureThy.thms_containing_consts;
authorwenzelm
Sat, 15 Mar 2008 18:07:58 +0100
changeset 26277 461e11226111
parent 26276 3386bb568550
child 26278 f0c6839df608
removed obsolete PureThy.thms_containing_consts;
src/HOL/Import/shuffler.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Import/shuffler.ML	Sat Mar 15 08:11:17 2008 +0100
+++ b/src/HOL/Import/shuffler.ML	Sat Mar 15 18:07:58 2008 +0100
@@ -623,10 +623,9 @@
     let
         val shuffles = ShuffleData.get thy
         val ignored = collect_ignored shuffles []
-        val rel_consts = term_consts t \\ ignored
-        val pot_thms = PureThy.thms_containing_consts thy rel_consts
+        val all_thms = map (`PureThy.get_name_hint) (maps #2 (Facts.dest (PureThy.all_facts_of thy)))
     in
-        List.filter (match_consts ignored t) pot_thms
+        List.filter (match_consts ignored t) all_thms
     end
 
 fun gen_shuffle_tac thy search thms i st =
isabelle