--- a/src/Doc/Classes/Setup.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/Doc/Classes/Setup.thy Sat Jan 05 17:24:33 2019 +0100
@@ -18,18 +18,18 @@
fun alpha_ast_tr [] = Ast.Variable "'a"
| alpha_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
fun alpha_ofsort_ast_tr [ast] =
- Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'a", ast]
+ Ast.Appl [Ast.Constant \<^syntax_const>\<open>_ofsort\<close>, Ast.Variable "'a", ast]
| alpha_ofsort_ast_tr asts = raise Ast.AST ("alpha_ast_tr", asts);
fun beta_ast_tr [] = Ast.Variable "'b"
| beta_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
fun beta_ofsort_ast_tr [ast] =
- Ast.Appl [Ast.Constant @{syntax_const "_ofsort"}, Ast.Variable "'b", ast]
+ Ast.Appl [Ast.Constant \<^syntax_const>\<open>_ofsort\<close>, Ast.Variable "'b", ast]
| beta_ofsort_ast_tr asts = raise Ast.AST ("beta_ast_tr", asts);
in
- [(@{syntax_const "_alpha"}, K alpha_ast_tr),
- (@{syntax_const "_alpha_ofsort"}, K alpha_ofsort_ast_tr),
- (@{syntax_const "_beta"}, K beta_ast_tr),
- (@{syntax_const "_beta_ofsort"}, K beta_ofsort_ast_tr)]
+ [(\<^syntax_const>\<open>_alpha\<close>, K alpha_ast_tr),
+ (\<^syntax_const>\<open>_alpha_ofsort\<close>, K alpha_ofsort_ast_tr),
+ (\<^syntax_const>\<open>_beta\<close>, K beta_ast_tr),
+ (\<^syntax_const>\<open>_beta_ofsort\<close>, K beta_ofsort_ast_tr)]
end
\<close>