--- a/src/Doc/IsarImplementation/Prelim.thy Wed Mar 12 22:41:04 2014 +0100
+++ b/src/Doc/IsarImplementation/Prelim.thy Wed Mar 12 22:44:55 2014 +0100
@@ -1056,6 +1056,14 @@
text {* This illustrates a key virtue of formalized bindings as
opposed to raw specifications of base names: the system can use this
additional information for feedback given to the user (error
- messages etc.). *}
+ messages etc.).
+
+ \medskip The following example refers to its source position
+ directly, which is occasionally useful for experimentation and
+ diagnostic purposes: *}
+
+ML_command {*
+ warning ("Look here" ^ Position.here @{here})
+*}
end