added comment: print translations do not mark tokens;

--- a/src/HOL/Hoare/Hoare.thy	Sat Mar 01 20:09:50 1997 +0100
+++ b/src/HOL/Hoare/Hoare.thy	Mon Mar 03 13:50:40 1997 +0100
@@ -151,6 +151,8 @@
 
 (*** print translations: semantics -> syntax ***)
 
+(* Note: does not mark tokens *)
+
 (* term_tr':term (name:string,trm:term) ersetzt in trm alle Vorkommen von name $ pvar durch
    entsprechende freie Variablen, welche die pvarID zu pvar darstellen. Beispiel:
         bei name="s" und dem Term "s(0)=s(Suc(0)) & s(0)=X" wird der Term "a=b & a=X" geliefert *)