Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned comments;
authorwenzelm
Tue, 06 Sep 2005 16:59:54 +0200
changeset 17279 7cd0099ae9bc
parent 17278 f27456a2a975
child 17280 a6917ddc864f
tuned comments;
src/HOL/Tools/res_axioms.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle