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