src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Mar 01 08:00:51 2023 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Wed Mar 01 08:00:51 2023 +0100
@@ -530,7 +530,7 @@
      one_line_proof_text ctxt num_chained) one_line_params
 
 fun abduce_text ctxt tms =
-  "Candidate" ^ plural_s (length tms) ^ " for missing hypothesis:\n" ^
+  "Candidate missing assumption" ^ plural_s (length tms) ^ ":\n" ^
   cat_lines (map (Syntax.string_of_term ctxt) tms)
 
 end;