# HG changeset patch
# User wenzelm
# Date 1286655500 -3600
# Node ID 6d54a48c859de7dd3a6dfe93a850709c45ae8808
# Parent  1080dee73a5332aa9fbb008d10a78545fdee8b27
more examples;

diff -r 1080dee73a53 -r 6d54a48c859d doc-src/IsarImplementation/Thy/Prelim.thy
--- a/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Oct 09 21:04:03 2010 +0100
+++ b/doc-src/IsarImplementation/Thy/Prelim.thy	Sat Oct 09 21:18:20 2010 +0100
@@ -1056,4 +1056,22 @@
   \end{description}
 *}
 
+text %mlex {* The following example yields the source position of some
+  concrete binding inlined into the text.
+*}
+
+ML {* Binding.pos_of @{binding here} *}
+
+text {* \medskip That position can be also printed in a message as
+  follows. *}
+
+ML_command {*
+  writeln
+    ("Look here" ^ Position.str_of (Binding.pos_of @{binding here}))
+*}
+
+text {* \noindent This illustrates a key virtue of formalized bindings
+  as opposed to raw specifications of base names: the system can use
+  this additional information for advanced feedback given to the user. *}
+
 end