# HG changeset patch
# User wenzelm
# Date 1413878425 -7200
# Node ID bb55a3530709db04fc54e38c257c3a7599957b8e
# Parent  6e7b009e6d94a6a247b75c009f7f4c73d7b23050
tuned spacing;

diff -r 6e7b009e6d94 -r bb55a3530709 src/Doc/Implementation/Prelim.thy
--- a/src/Doc/Implementation/Prelim.thy	Tue Oct 21 09:50:22 2014 +0200
+++ b/src/Doc/Implementation/Prelim.thy	Tue Oct 21 10:00:25 2014 +0200
@@ -1048,10 +1048,9 @@
 text \<open>\medskip That position can be also printed in a message as
   follows:\<close>
 
-ML_command \<open>
-  writeln
-    ("Look here" ^ Position.here (Binding.pos_of @{binding here}))
-\<close>
+ML_command
+  \<open>writeln
+    ("Look here" ^ Position.here (Binding.pos_of @{binding here}))\<close>
 
 text \<open>This illustrates a key virtue of formalized bindings as
   opposed to raw specifications of base names: the system can use this
@@ -1062,8 +1061,6 @@
   directly, which is occasionally useful for experimentation and
   diagnostic purposes:\<close>
 
-ML_command \<open>
-  warning ("Look here" ^ Position.here @{here})
-\<close>
+ML_command \<open>warning ("Look here" ^ Position.here @{here})\<close>
 
 end