diff -r ce754ad78bc9 -r c0cae24b9d46 ProgTutorial/antiquote_setup.ML
--- a/ProgTutorial/antiquote_setup.ML	Fri Oct 02 15:38:14 2009 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Sat Oct 03 13:01:39 2009 +0200
@@ -63,6 +63,13 @@
 val output_struct = gen_output_struct (K output)
 val output_struct_ind = gen_output_struct output_indexed
 
+(* prints functors; no checks *)
+fun gen_output_funct outfn {context = ctxt, ...} txt = 
+  (outfn {main = Code txt, minor = Plain "functor"} (split_lines txt))
+
+val output_funct = gen_output_funct (K output)
+val output_funct_ind = gen_output_funct output_indexed
+
 (* checks and prints types *)
 fun gen_output_type outfn {context = ctxt, ...} txt = 
   (eval_fn ctxt (ml_type txt); 
@@ -95,6 +102,8 @@
 val _ = ThyOutput.antiquotation "ML_type_ind" single_arg output_type_ind
 val _ = ThyOutput.antiquotation "ML_struct" single_arg output_struct
 val _ = ThyOutput.antiquotation "ML_struct_ind" single_arg output_struct_ind
+val _ = ThyOutput.antiquotation "ML_funct" single_arg output_funct
+val _ = ThyOutput.antiquotation "ML_funct_ind" single_arg output_funct_ind
 val _ = ThyOutput.antiquotation "ML_response" two_args output_response
 val _ = ThyOutput.antiquotation "ML_response_fake" two_args output_response_fake
 val _ = ThyOutput.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both