--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jun 22 18:31:49 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Tue Jun 22 18:47:45 2010 +0200
@@ -20,6 +20,7 @@
open Sledgehammer_Util
open Sledgehammer_Fact_Preprocessor
+open Sledgehammer_HOL_Clause
open Sledgehammer_Proof_Reconstruct
open ATP_Manager
@@ -125,8 +126,7 @@
\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 full_types i n [])
+ handle TRIVIAL () => (SOME [], metis_line full_types i n [])
| ERROR msg => (NONE, "Error: " ^ msg)
end