# HG changeset patch
# User wenzelm
# Date 1205600878 -3600
# Node ID 461e11226111292b3a6d5c5736830ae97fb6e5b1
# Parent  3386bb568550110d3c051a72c3b987ee12eddfe1
removed obsolete PureThy.thms_containing_consts;

diff -r 3386bb568550 -r 461e11226111 src/HOL/Import/shuffler.ML
--- 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 =