--- a/src/HOLCF/IOA/Modelcheck/Cockpit.ML	Thu Apr 07 09:24:35 2005 +0200
+++ b/src/HOLCF/IOA/Modelcheck/Cockpit.ML	Thu Apr 07 09:25:33 2005 +0200
@@ -15,7 +15,7 @@
 qed"cockpit_implements_Info_while_Al";
 
 (* to prove that before any alarm arrives (and after each acknowledgment),
-   info remains at NONE *)
+   info remains at None *)
 Goal "cockpit =<| Info_before_Al";
 by (is_sim_tac aut_simps 1);       
 qed"cockpit_implements_Info_before_Al";