author | mengj |
Sat, 30 Sep 2006 14:31:02 +0200 | |
changeset 20789 | e279499c4f80 |
parent 20788 | d51711512d07 |
child 20790 | a9595fdc02b1 |
--- 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 [];