src/HOL/Tools/ATP/atp_util.ML

     end
   | extract_lambda_def _ _ = raise Fail "malformed lifted lambda"
 
 fun short_thm_name ctxt th =
   let
-    val long = Thm.get_name_hint th
+    val long = Thm_Name.short (Thm.get_name_hint th)
     val short = Long_Name.base_name long
   in
     (case try (singleton (Attrib.eval_thms ctxt)) (Facts.named short, []) of
       SOME th' => if Thm.eq_thm_prop (th, th') then short else long
     | _ => long)