author | wenzelm |
Tue, 04 Dec 2001 18:10:49 +0100 | |
changeset 12362 | 57cd572103c4 |
parent 12361 | b7ca18198669 |
child 12363 | a1784e56d8d6 |
--- 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;