# HG changeset patch
# User mengj
# Date 1159619462 -7200
# Node ID e279499c4f803c3b2cde7d5811a663bb62596e8b
# Parent  d51711512d0729b1b47cf830d5e737e9d39059f4
Removed ResHolClause.LAM2COMB exception.

diff -r d51711512d07 -r e279499c4f80 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Sat Sep 30 14:29:52 2006 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Sat Sep 30 14:31:02 2006 +0200
@@ -591,7 +591,6 @@
   | cnf_rules_pairs_aux pairs ((name,th)::ths) =
       let val pairs' = (pair_name_cls 0 (name, cnf_axiom(name,th))) @ pairs
                        handle THM _ => pairs | ResClause.CLAUSE _ => pairs
-                            | ResHolClause.LAM2COMB _ => pairs
       in  cnf_rules_pairs_aux pairs' ths  end;
 
 val cnf_rules_pairs = cnf_rules_pairs_aux [];