src/HOLCF/IOA/NTP/Sender.ML

 \ R_ack(b) : actions(sender_asig)    &   \
 \ C_m_s : actions(sender_asig)          &   \
 \ C_m_r ~: actions(sender_asig)         &   \
 \ C_r_s : actions(sender_asig)          &   \
 \ C_r_r(m) ~: actions(sender_asig)";
-by(simp_tac (!simpset addsimps 
+by(simp_tac (simpset() addsimps 
              (Sender.sender_asig_def :: actions_def :: 
               asig_projections)) 1);
 qed "in_sender_asig";
 
 val sender_projections =