--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri Apr 23 19:26:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri Apr 23 19:36:49 2010 +0200
@@ -123,9 +123,8 @@
\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;