--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Oct 17 20:03:37 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Thu Oct 17 20:20:53 2013 +0200
@@ -1201,7 +1201,7 @@
in
if verbose orelse auto_level < 2 then
"Learned " ^ string_of_int n ^ " nontrivial " ^
- (if run_prover then "automatic" else "Isar") ^ " proof" ^ plural_s n ^
+ (if run_prover then "automatic and " else "") ^ "Isar proof" ^ plural_s n ^
(if verbose then " in " ^ string_of_time (Timer.checkRealTimer timer)
else "") ^ "."
else