diff -r 97c6787099bc -r d49bf150c925 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Wed Jan 09 08:04:03 2008 +0100
+++ b/doc-src/IsarRef/generic.tex	Wed Jan 09 08:04:40 2008 +0100
@@ -555,7 +555,7 @@
   $\FIXESNAME$ in $body$ are lifted to the global theory level
   (\emph{class operations} $\vec f$ of class $c$),
   mapping the local type parameter $\alpha$ to a schematic
-  type variable $?\alpha::c$
+  type variable $?\alpha::c$.
   $\ASSUMESNAME$ in $body$ are also lifted, mapping each local parameter
   $f::\tau [\alpha]$ to its corresponding global constant
   $f::\tau [?\alpha::c]$.
@@ -606,6 +606,9 @@
     by theory-level constants $g [?\alpha::c]$ referring to theory-level
     class operations $\vec f [?\alpha::c]$
   \item Local theorem bindings are lifted as are assumptions.
+  \item Local syntax refers to local operations $g [\alpha]$ and
+    global operations $g [?\alpha::c]$ uniformly.  Type inference
+    resolves ambiguities;  in rare cases, manual type annotations are needed.
 \end{itemize}