--- 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 *}