src/HOL/Hoare_Parallel/Quote_Antiquote.thy

--- a/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Thu Feb 11 22:06:37 2010 +0100
+++ b/src/HOL/Hoare_Parallel/Quote_Antiquote.thy	Thu Feb 11 22:19:58 2010 +0100
@@ -16,9 +16,9 @@
 
 parse_translation {*
   let
-    fun quote_tr [t] = Syntax.quote_tr "_antiquote" t
+    fun quote_tr [t] = Syntax.quote_tr @{syntax_const "_antiquote"} t
       | quote_tr ts = raise TERM ("quote_tr", ts);
-  in [("_quote", quote_tr)] end
+  in [(@{syntax_const "_quote"}, quote_tr)] end
 *}
 
 end
\ No newline at end of file