diff -r 3a1aef73b2b2 -r aea5d7fa7ef5 doc-src/Classes/Thy/Setup.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Classes/Thy/Setup.thy	Wed Mar 04 11:05:29 2009 +0100
@@ -0,0 +1,34 @@
+theory Setup
+imports Main Code_Integer
+uses
+  "../../antiquote_setup"
+  "../../more_antiquote"
+begin
+
+ML {* Code_Target.code_width := 74 *}
+
+syntax
+  "_alpha" :: "type"  ("\<alpha>")
+  "_alpha_ofsort" :: "sort \<Rightarrow> type"  ("\<alpha>()\<Colon>_" [0] 1000)
+  "_beta" :: "type"  ("\<beta>")
+  "_beta_ofsort" :: "sort \<Rightarrow> type"  ("\<beta>()\<Colon>_" [0] 1000)
+
+parse_ast_translation {*
+  let
+    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]
+      | 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]
+      | 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
+*}
+
+end
\ No newline at end of file