diff -r c7f04a008c9c -r 043ef82000b4 CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Wed Mar 18 03:03:51 2009 +0100
+++ b/CookBook/FirstSteps.thy	Wed Mar 18 03:27:15 2009 +0100
@@ -897,8 +897,7 @@
    shows "Q t" (*<*)oops(*>*) 
 
 text {*
-  The corresponding ML-code is as follows:\footnote{Note that @{text "|>"} is reverse
-  application. See Section~\ref{sec:combinators}.}
+  The corresponding ML-code is as follows:
 
 @{ML_response_fake [display,gray]
 "let