--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed May 28 10:04:28 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Wed May 28 12:34:26 2014 +0200
@@ -192,8 +192,7 @@
val auto_try_max_facts_divisor = 2 (* FUDGE *)
fun string_of_facts facts =
- "Including " ^ string_of_int (length facts) ^
- " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
+ "Including " ^ string_of_int (length facts) ^ " relevant fact" ^ plural_s (length facts) ^ ":\n" ^
(facts |> map (fst o fst) |> space_implode " ") ^ "."
fun string_of_factss factss =