src/HOL/Import/shuffler.ML
changeset 27173 9ae98c3cd3d6
parent 26939 1035c89b4c02
child 27330 1af2598b5f7d
     1.1 --- a/src/HOL/Import/shuffler.ML	Thu Jun 12 15:49:25 2008 +0200
     1.2 +++ b/src/HOL/Import/shuffler.ML	Thu Jun 12 16:41:47 2008 +0200
     1.3 @@ -624,7 +624,7 @@
     1.4          val shuffles = ShuffleData.get thy
     1.5          val ignored = collect_ignored shuffles []
     1.6          val all_thms =
     1.7 -          map (`PureThy.get_name_hint) (maps #2 (Facts.dest_static (PureThy.facts_of thy)))
     1.8 +          map (`PureThy.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy)))
     1.9      in
    1.10          List.filter (match_consts ignored t) all_thms
    1.11      end