--- a/src/HOL/IOA/NTP/Receiver.ML	Sun Nov 12 16:29:12 1995 +0100
+++ b/src/HOL/IOA/NTP/Receiver.ML	Mon Nov 13 12:06:57 1995 +0100
@@ -16,7 +16,7 @@
 \ C_r_s ~: actions(receiver_asig)         &   \
 \ C_r_r(m) : actions(receiver_asig)";
   by(simp_tac (!simpset addsimps (Receiver.receiver_asig_def :: actions_def :: 
-                                  asig_projections @ set_lemmas)) 1);
+                                  asig_projections)) 1);
 qed "in_receiver_asig";
 
 val receiver_projections =