# HG changeset patch
# User blanchet
# Date 1277472132 -7200
# Node ID de5feddaa95cb756a0144504ab40403b5ad3ac2d
# Parent  931f5948a32dfd17b34fb6496c576707ebadc177
got rid of needless exception

diff -r 931f5948a32d -r de5feddaa95c src/HOL/Tools/Sledgehammer/sledgehammer_fact_preprocessor.ML
--- 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
 
diff -r 931f5948a32d -r de5feddaa95c src/HOL/Tools/Sledgehammer/sledgehammer_fol_clause.ML
--- 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
diff -r 931f5948a32d -r de5feddaa95c src/HOL/Tools/Sledgehammer/sledgehammer_hol_clause.ML
--- 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)