fix due to new neq_simproc
authornipkow
Sat, 08 Oct 2005 15:20:58 +0200
changeset 17790 aa6ec0efe4d3
parent 17789 ccba4e900023
child 17791 f4453001cbde
fix due to new neq_simproc
src/HOLCF/IOA/NTP/Multiset.ML
--- a/src/HOLCF/IOA/NTP/Multiset.ML	Fri Oct 07 23:29:00 2005 +0200
+++ b/src/HOLCF/IOA/NTP/Multiset.ML	Sat Oct 08 15:20:58 2005 +0200
@@ -68,7 +68,7 @@
   by (asm_simp_tac (simpset() addsimps 
                       [count_addm_simp,Multiset.delm_nonempty_def,
                        Multiset.countm_nonempty_def,pos_count_imp_pos_countm]) 1);
-  by (asm_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
+  by (Auto_tac);
 qed "countm_done_delm";