src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML

         (NONE, "Failure: No proof was found with the current time limit. You \
                \can increase the time limit using the \"timeout\" \
                \option (e.g., \"timeout = " ^
                string_of_int (10 + msecs div 1000) ^ " s\").")
     | {message, ...} => (NONE, "ATP error: " ^ message))
-    handle Sledgehammer_HOL_Clause.TRIVIAL =>
-        (SOME [], metis_line i n [])
-      | ERROR msg => (NONE, "Error: " ^ msg)
+    handle Sledgehammer_HOL_Clause.TRIVIAL => (SOME [], metis_line i n [])
+         | ERROR msg => (NONE, "Error: " ^ msg)
   end
 
 end;