1.1 --- a/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:45 2012 +0200
     1.2 +++ b/src/HOL/TPTP/mash_eval.ML	Fri Jul 20 22:19:45 2012 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4  
     1.5  val all_names =
     1.6    filter_out is_likely_tautology_or_too_meta
     1.7 -  #> map (rpair () o Thm.get_name_hint) #> Symtab.make
     1.8 +  #> map (rpair () o nickname_of) #> Symtab.make
     1.9  
    1.10  fun evaluate_mash_suggestions ctxt params thy file_name =
    1.11    let
    1.12 @@ -70,7 +70,7 @@
    1.13        let
    1.14          val (name, suggs) = extract_query line
    1.15          val th =
    1.16 -          case find_first (fn (_, th) => Thm.get_name_hint th = name) facts of
    1.17 +          case find_first (fn (_, th) => nickname_of th = name) facts of
    1.18              SOME (_, th) => th
    1.19            | NONE => error ("No fact called \"" ^ name ^ "\"")
    1.20          val goal = goal_of_thm thy th