removed obsolete PureThy.thms_containing_consts;
authorwenzelm
Sat Mar 15 18:07:58 2008 +0100 (2008-03-15)
changeset 26277461e11226111
parent 26276 3386bb568550
child 26278 f0c6839df608
removed obsolete PureThy.thms_containing_consts;
src/HOL/Import/shuffler.ML
     1.1 --- a/src/HOL/Import/shuffler.ML	Sat Mar 15 08:11:17 2008 +0100
     1.2 +++ b/src/HOL/Import/shuffler.ML	Sat Mar 15 18:07:58 2008 +0100
     1.3 @@ -623,10 +623,9 @@
     1.4      let
     1.5          val shuffles = ShuffleData.get thy
     1.6          val ignored = collect_ignored shuffles []
     1.7 -        val rel_consts = term_consts t \\ ignored
     1.8 -        val pot_thms = PureThy.thms_containing_consts thy rel_consts
     1.9 +        val all_thms = map (`PureThy.get_name_hint) (maps #2 (Facts.dest (PureThy.all_facts_of thy)))
    1.10      in
    1.11 -        List.filter (match_consts ignored t) pot_thms
    1.12 +        List.filter (match_consts ignored t) all_thms
    1.13      end
    1.14  
    1.15  fun gen_shuffle_tac thy search thms i st =