# HG changeset patch
# User wenzelm
# Date 1007485849 -3600
# Node ID 57cd572103c4a363020a30027f7855e8987f0740
# Parent  b7ca1819866914c2a6ba8b4d71e3796a5c5b2794
made SML/NJ happy;

diff -r b7ca18198669 -r 57cd572103c4 src/Provers/classical.ML
--- 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;