# HG changeset patch
# User mengj
# Date 1144379543 -7200
# Node ID 36b6b15ee6707dd636d8f06a8b5a18b02eb81fb4
# Parent  1a07f6cf1e6c71ec932011ae981d33127accbaf8
added another function for CNF.

diff -r 1a07f6cf1e6c -r 36b6b15ee670 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Fri Apr 07 05:12:00 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Fri Apr 07 05:12:23 2006 +0200
@@ -26,13 +26,13 @@
   val skolem_thm : thm -> thm list
   val cnf_rules1 : (string * thm) list -> string list -> (string * thm list) list * string list
   val cnf_rules2 : (string * thm) list -> string list -> (string * term list) list * string list
+  val cnf_rules_pairs : (string * Thm.thm) list -> (Thm.thm * (string * int)) list list;
   val clausify_rules_pairs_abs : (string * thm) list -> (Term.term * (string * int)) list list
   val meson_method_setup : theory -> theory
   val setup : theory -> theory
 
   val atpset_rules_of_thy : theory -> (string * thm) list
   val atpset_rules_of_ctxt : Proof.context -> (string * thm) list
-
   end;
 
 structure ResAxioms : RES_AXIOMS =
@@ -403,6 +403,21 @@
 	((name,map prop_of (cnf_axiom (name,th))) :: ts,es) handle _ => (ts,(name::es)) 
       end;
 
+
+fun cnf_rules_pairs_aux [] = []
+  | cnf_rules_pairs_aux ((name,th)::ths) =
+    let val ts = cnf_rules_pairs_aux ths
+	fun pair_name_cls k (n, []) = []
+	  | pair_name_cls k (n, cls::clss) =
+	    (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 cnf_rules_pairs thms = rev (cnf_rules_pairs_aux thms);
+
 fun clausify_rules_pairs_abs_aux [] = []
   | clausify_rules_pairs_abs_aux ((name,th)::ths) =
       let val ts = clausify_rules_pairs_abs_aux ths