diff -r 253ea99c1441 -r cb39c41548bd CookBook/Tactical.thy
--- a/CookBook/Tactical.thy	Thu Feb 26 12:16:24 2009 +0000
+++ b/CookBook/Tactical.thy	Thu Feb 26 14:20:52 2009 +0000
@@ -1481,7 +1481,8 @@
   The reason for this behaviour is that @{text "(op \<or>)"} expects two
   arguments.  So the term must be of the form @{text "(Const \<dots> $ t1) $ t2"}. The
   conversion is then applied to @{text "t2"} which in the example above
-  stands for @{term "True \<and> Q"}.
+  stands for @{term "True \<and> Q"}. The function @{ML Conv.fun_conv} applies
+  the conversion to the first argument of an application.
 
   The function @{ML Conv.abs_conv} applies a conversion under an abstractions.
   For example: