src/HOL/Import/shuffler.ML
changeset 26662 39483503705f
parent 26424 a6cad32a27b0
child 26690 e30b8d500c7d
     1.1 --- a/src/HOL/Import/shuffler.ML	Tue Apr 15 18:49:13 2008 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Tue Apr 15 18:49:15 2008 +0200
     1.3 @@ -623,7 +623,8 @@
     1.4      let
     1.5          val shuffles = ShuffleData.get thy
     1.6          val ignored = collect_ignored shuffles []
     1.7 -        val all_thms = map (`PureThy.get_name_hint) (maps #2 (Facts.dest (PureThy.all_facts_of thy)))
     1.8 +        val all_thms =
     1.9 +          map (`PureThy.get_name_hint) (maps #2 (Facts.dest_table (PureThy.facts_of thy)))
    1.10      in
    1.11          List.filter (match_consts ignored t) all_thms
    1.12      end