diff -r f4bb3068d819 -r 22b87ab47d3b src/Doc/Classes/Classes.thy
--- a/src/Doc/Classes/Classes.thy	Thu Oct 30 23:14:11 2014 +0100
+++ b/src/Doc/Classes/Classes.thy	Fri Oct 31 11:18:17 2014 +0100
@@ -179,8 +179,7 @@
   primrec declaration; by default, the local name of a class operation
   @{text f} to be instantiated on type constructor @{text \<kappa>} is
   mangled as @{text f_\<kappa>}.  In case of uncertainty, these names may be
-  inspected using the @{command "print_context"} command or the
-  corresponding ProofGeneral button.
+  inspected using the @{command "print_context"} command.
 *}
 
 subsection {* Lifting and parametric types *}