--- a/doc-src/Classes/Thy/Setup.thy Thu Feb 11 22:06:37 2010 +0100
+++ b/doc-src/Classes/Thy/Setup.thy Thu Feb 11 22:19:58 2010 +0100
@@ -18,17 +18,19 @@
fun alpha_ast_tr [] = Syntax.Variable "'a"
| alpha_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
fun alpha_ofsort_ast_tr [ast] =
- Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'a", ast]
+ Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'a", ast]
| alpha_ofsort_ast_tr asts = raise Syntax.AST ("alpha_ast_tr", asts);
fun beta_ast_tr [] = Syntax.Variable "'b"
| beta_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
fun beta_ofsort_ast_tr [ast] =
- Syntax.Appl [Syntax.Constant "_ofsort", Syntax.Variable "'b", ast]
+ Syntax.Appl [Syntax.Constant @{syntax_const "_ofsort"}, Syntax.Variable "'b", ast]
| beta_ofsort_ast_tr asts = raise Syntax.AST ("beta_ast_tr", asts);
- in [
- ("_alpha", alpha_ast_tr), ("_alpha_ofsort", alpha_ofsort_ast_tr),
- ("_beta", beta_ast_tr), ("_beta_ofsort", beta_ofsort_ast_tr)
- ] end
+ in
+ [(@{syntax_const "_alpha"}, alpha_ast_tr),
+ (@{syntax_const "_alpha_ofsort"}, alpha_ofsort_ast_tr),
+ (@{syntax_const "_beta"}, beta_ast_tr),
+ (@{syntax_const "_beta_ofsort"}, beta_ofsort_ast_tr)]
+ end
*}
end
\ No newline at end of file