--- a/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 06:14:37 2010 +0100
+++ b/src/HOL/Tools/ATP_Manager/atp_minimal.ML Fri Mar 19 13:02:18 2010 +0100
@@ -14,7 +14,7 @@
(string * thm list) list -> ((string * thm list) list * int) option * string
end
-structure ATP_Minimal: ATP_MINIMAL =
+structure ATP_Minimal : ATP_MINIMAL =
struct
(* Linear minimization *)
@@ -170,7 +170,7 @@
(NONE, "Error in prover: " ^ msg)
| (Failure, _) =>
(NONE, "Failure: No proof with the theorems supplied"))
- handle Sledgehammer_HOL_Clause.TOO_TRIVIAL =>
+ handle Sledgehammer_HOL_Clause.TRIVIAL =>
(SOME ([], 0), "Trivial: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
| ERROR msg => (NONE, "Error: " ^ msg)
end