--- a/src/HOL/ex/Antiquote.thy Fri Apr 08 11:39:45 2011 +0200
+++ b/src/HOL/ex/Antiquote.thy Fri Apr 08 13:31:16 2011 +0200
@@ -25,11 +25,13 @@
where "Expr exp env = exp env"
parse_translation {*
- [Syntax.quote_antiquote_tr @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
+ [Syntax_Trans.quote_antiquote_tr
+ @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
*}
print_translation {*
- [Syntax.quote_antiquote_tr' @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
+ [Syntax_Trans.quote_antiquote_tr'
+ @{syntax_const "_Expr"} @{const_syntax var} @{const_syntax Expr}]
*}
term "EXPR (a + b + c)"