changeset 27865 | 27a8ad9612a3 |
parent 27330 | 1af2598b5f7d |
child 28397 | 389c5e494605 |
--- a/src/HOL/Import/shuffler.ML Thu Aug 14 11:55:05 2008 +0200 +++ b/src/HOL/Import/shuffler.ML Thu Aug 14 16:52:46 2008 +0200 @@ -627,7 +627,7 @@ val shuffles = ShuffleData.get thy val ignored = collect_ignored shuffles [] val all_thms = - map (`PureThy.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy))) + map (`Thm.get_name_hint) (maps #2 (Facts.dest_static [] (PureThy.facts_of thy))) in List.filter (match_consts ignored t) all_thms end