--- a/src/HOL/Tools/res_axioms.ML Tue Sep 06 16:59:53 2005 +0200
+++ b/src/HOL/Tools/res_axioms.ML Tue Sep 06 16:59:54 2005 +0200
@@ -368,7 +368,7 @@
fun cnf_rules [] err_list = ([],err_list)
| cnf_rules ((name,th) :: thms) err_list =
let val (ts,es) = cnf_rules thms err_list
- in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end;
+ in (cnf_axiom (name,th) :: ts,es) handle _ => (ts, (th::es)) end; (* FIXME avoid handle _ *)
(**** Convert all theorems of a claset/simpset into clauses (ResClause.clause) ****)
@@ -392,7 +392,7 @@
let val (ts,es) = clausify_rules_pairs thms err_list
in
((clausify_axiom_pairs (name,thm))::ts, es)
- handle _ => (ts, (thm::es))
+ handle _ => (ts, (thm::es)) (* FIXME avoid handle _ *)
end;