src/HOL/Import/shuffler.ML

 fun find_potential thy t =
     let
         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
 
 fun gen_shuffle_tac thy search thms i st =