# HG changeset patch
# User wenzelm
# Date 1126018794 -7200
# Node ID 7cd0099ae9bc0d8bd0acd3819395a1c0e6c62a0a
# Parent  f27456a2a975658868fe8bc822a29a5abab98297
tuned comments;

diff -r f27456a2a975 -r 7cd0099ae9bc src/HOL/Tools/res_axioms.ML
--- 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;