diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Isar_Examples/Hoare.thy
--- a/src/HOL/Isar_Examples/Hoare.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Isar_Examples/Hoare.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -185,8 +185,8 @@
   of the concrete syntactic representation of our Hoare language, the
   actual ``ML drivers'' is quite involved.  Just note that the we
   re-use the basic quote/antiquote translations as already defined in
-  Isabelle/Pure (see \verb,Syntax.quote_tr, and
-  \verb,Syntax.quote_tr',). *}
+  Isabelle/Pure (see @{ML Syntax_Trans.quote_tr}, and
+  @{ML Syntax_Trans.quote_tr'},). *}
 
 syntax
   "_quote"       :: "'b => ('a => 'b)"       ("(.'(_').)" [0] 1000)
@@ -215,7 +215,7 @@
 
 parse_translation {*
   let
-    fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t
+    fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
       | quote_tr ts = raise TERM ("quote_tr", ts);
   in [(@{syntax_const "_quote"}, quote_tr)] end
 *}
@@ -228,7 +228,7 @@
 print_translation {*
   let
     fun quote_tr' f (t :: ts) =
-          Term.list_comb (f $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
+          Term.list_comb (f $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
       | quote_tr' _ _ = raise Match;
 
     val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
@@ -238,8 +238,8 @@
       | bexp_tr' _ _ = raise Match;
 
     fun assign_tr' (Abs (x, _, f $ k $ Bound 0) :: ts) =
-          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax.update_name_tr' f)
-            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
+          quote_tr' (Syntax.const @{syntax_const "_Assign"} $ Syntax_Trans.update_name_tr' f)
+            (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
       | assign_tr' _ = raise Match;
   in
    [(@{const_syntax Collect}, assert_tr'),