# HG changeset patch
# User paulson
# Date 1141746471 -3600
# Node ID 79053aa24abfc0a5e37760a67040e990591585c1
# Parent  4ec788c69f8291542462b0c33e938e1336fdc39e
Tidying. clausify_rules_pairs_abs now returns clauses in the same order as before.
Removal of the unused err_list.

diff -r 4ec788c69f82 -r 79053aa24abf src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Tue Mar 07 16:46:54 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML	Tue Mar 07 16:47:51 2006 +0100
@@ -393,27 +393,28 @@
 
 fun cnf_rules1 [] err_list = ([],err_list)
   | cnf_rules1 ((name,th) :: ths) err_list =
-    let val (ts,es) = cnf_rules1 ths err_list
-    in
-	((name,cnf_axiom (name,th)) :: ts,es) handle _ => (ts,(name::es)) end;
+      let val (ts,es) = cnf_rules1 ths err_list
+      in ((name,cnf_axiom (name,th)) :: ts,es) handle _ => (ts,(name::es)) end;
 
 fun cnf_rules2 [] err_list = ([],err_list)
   | cnf_rules2 ((name,th) :: ths) err_list =
-    let val (ts,es) = cnf_rules2 ths err_list
-    in
-	((name,map prop_of (cnf_axiom (name,th))) :: ts,es) handle _ => (ts,(name::es)) end;
+      let val (ts,es) = cnf_rules2 ths err_list
+      in
+	((name,map prop_of (cnf_axiom (name,th))) :: ts,es) handle _ => (ts,(name::es)) 
+      end;
 
-fun clausify_rules_pairs_abs_aux [] err_list = ([],err_list)
-  | clausify_rules_pairs_abs_aux ((name,th)::ths) err_list =
-    let val (ts,es) = clausify_rules_pairs_abs_aux ths err_list
-	fun pair_name_cls k (n, []) = []
-	  | pair_name_cls k (n, (cls::clss)) =
-	    (prop_of cls,(n,k))::(pair_name_cls (k + 1) (n, clss))
-    in
-	(pair_name_cls 0 (name,(cnf_axiom(name,th)))::ts,es) handle _ => (ts,(name::es))
-    end;
+fun clausify_rules_pairs_abs_aux [] = []
+  | clausify_rules_pairs_abs_aux ((name,th)::ths) =
+      let val ts = clausify_rules_pairs_abs_aux ths
+	  fun pair_name_cls k (n, []) = []
+	    | pair_name_cls k (n, cls::clss) =
+		(prop_of cls, (n,k)) :: (pair_name_cls (k+1) (n, clss))
+      in
+	  pair_name_cls 0 (name, (cnf_axiom(name,th))) :: ts
+	  handle THM _ => ts | ResClause.CLAUSE _ => ts | ResHolClause.LAM2COMB _ => ts
+      end;
 
-fun clausify_rules_pairs_abs thms = fst (clausify_rules_pairs_abs_aux thms []);
+fun clausify_rules_pairs_abs thms = rev (clausify_rules_pairs_abs_aux thms);
 
 
 (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)