1.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Nov 10 19:04:18 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Fri Nov 10 20:58:48 2006 +0100
     1.3 @@ -647,7 +647,8 @@
     1.4                         handle THM _ => pairs | ResClause.CLAUSE _ => pairs
     1.5        in  cnf_rules_pairs_aux pairs' ths  end;
     1.6  
     1.7 -val cnf_rules_pairs = cnf_rules_pairs_aux [];
     1.8 +(*The combination of rev and tail recursion preserves the original order*)
     1.9 +fun cnf_rules_pairs l = cnf_rules_pairs_aux [] (rev l);
    1.10  
    1.11  
    1.12  (**** Convert all theorems of a claset/simpset into clauses (ResClause.clause, or ResHolClause.clause) ****)