src/HOL/Hoare_Parallel/Quote_Antiquote.thy

--- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Fri Apr 08 13:31:16 2011 +0200
@@ -16,7 +16,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
 *}