--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Jun 25 15:18:58 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML Fri Jun 25 15:22:12 2010 +0200
@@ -463,8 +463,7 @@
| do_all pairs ((name, th) :: ths) =
let
val new_pairs = do_one ((name, 0), th) (cnf_axiom thy th)
- handle THM _ => [] |
- CLAUSE _ => []
+ handle THM _ => []
in do_all (new_pairs @ pairs) ths end
in do_all [] o rev end
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Jun 25 15:18:58 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML Fri Jun 25 15:22:12 2010 +0200
@@ -39,7 +39,6 @@
datatype type_literal =
TyLitVar of string * name |
TyLitFree of string * name
- exception CLAUSE of string * term
val type_literals_for_types : typ list -> type_literal list
datatype arLit =
TConsLit of class * string * string list
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Jun 25 15:18:58 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML Fri Jun 25 15:22:12 2010 +0200
@@ -147,7 +147,7 @@
let val (P', tsP) = combterm_of thy P
val (Q', tsQ) = combterm_of thy Q
in (CombApp (P', Q'), union (op =) tsP tsQ) end
- | combterm_of _ (t as Abs _) = raise CLAUSE ("HOL clause", t)
+ | combterm_of _ (t as Abs _) = raise Fail "HOL clause: Abs"
fun predicate_of thy ((@{const Not} $ P), polarity) =
predicate_of thy (P, not polarity)