--- a/src/Pure/General/position.ML Thu Apr 10 18:29:32 2014 +0200
+++ b/src/Pure/General/position.ML Fri Apr 11 09:36:38 2014 +0200
@@ -191,7 +191,7 @@
Unsynchronized.change r (append (map (rpair "") reports));
-(* here: inlined formal markup *)
+(* here: user output *)
fun here pos =
let