src/Doc/Implementation/ML.thy

   @{assert} (a <> b);
 *}
 
 text {* \medskip See @{file "~~/src/Pure/Concurrent/mailbox.ML"} how
   to implement a mailbox as synchronized variable over a purely
-  functional queue. *}
+  functional list. *}
 
 
 section {* Managed evaluation *}
 
 text {* Execution of Standard ML follows the model of strict