--- a/src/HOL/Tools/atp_manager.ML Tue Nov 18 09:41:23 2008 +0100
+++ b/src/HOL/Tools/atp_manager.ML Tue Nov 18 11:26:59 2008 +0100
@@ -287,6 +287,10 @@
let
val _ = register birthtime deadtime (Thread.self (), desc)
val result = prover i proof_state
+ handle ResHolClause.TOO_TRIVIAL
+ => (true, "Empty clause: Try this command: " ^ Markup.markup Markup.sendback "apply metis")
+ | ERROR msg
+ => (false, "Error: " ^ msg)
val _ = priority (unregister result (Thread.self ()))
in () end handle Interrupt => ())
in () end);