src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Mon Jul 26 11:26:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Mon Jul 26 14:14:24 2010 +0200
@@ -126,8 +126,7 @@
                \option (e.g., \"timeout = " ^
                string_of_int (10 + msecs div 1000) ^ " s\").")
     | {message, ...} => (NONE, "ATP error: " ^ message))
-    handle TRIVIAL () => (SOME [], metis_line full_types i n [])
-         | ERROR msg => (NONE, "Error: " ^ msg)
+    handle ERROR msg => (NONE, "Error: " ^ msg)
   end
 
 end;