diff -r 25d9d836ed9c -r 326f57825e1a src/HOL/Hoare_Parallel/OG_Syntax.thy
--- a/src/HOL/Hoare_Parallel/OG_Syntax.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Hoare_Parallel/OG_Syntax.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -76,11 +76,11 @@
 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;
 
     fun annquote_tr' f (r :: t :: ts) =
-          Term.list_comb (f $ r $ Syntax.quote_tr' @{syntax_const "_antiquote"} t, ts)
+          Term.list_comb (f $ r $ Syntax_Trans.quote_tr' @{syntax_const "_antiquote"} t, ts)
       | annquote_tr' _ _ = raise Match;
 
     val assert_tr' = quote_tr' (Syntax.const @{syntax_const "_Assert"});
@@ -94,13 +94,13 @@
       | annbexp_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;
 
     fun annassign_tr' (r :: Abs (x, _, f $ k $ Bound 0) :: ts) =
-          quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax.update_name_tr' f)
-            (Abs (x, dummyT, Syntax.const_abs_tr' k) :: ts)
+          quote_tr' (Syntax.const @{syntax_const "_AnnAssign"} $ r $ Syntax_Trans.update_name_tr' f)
+            (Abs (x, dummyT, Syntax_Trans.const_abs_tr' k) :: ts)
       | annassign_tr' _ = raise Match;
 
     fun Parallel_PAR [(Const (@{const_syntax Cons}, _) $