| changeset 12362 | 57cd572103c4 |
| parent 12311 | ce5f9e61c037 |
| child 12376 | 480303e3fa08 |
--- a/src/Provers/classical.ML Tue Dec 04 18:00:11 2001 +0100 +++ b/src/Provers/classical.ML Tue Dec 04 18:10:49 2001 +0100 @@ -322,7 +322,7 @@ fun delete_tagged_list brls netpr = foldr delete_tagged_brl (brls, netpr); -val delete = delete_tagged_list o joinrules; +fun delete x = delete_tagged_list (joinrules x); val mem_thm = gen_mem eq_thm and rem_thm = gen_rem eq_thm;