--- a/ProgTutorial/antiquote_setup.ML	Tue Jun 28 08:44:34 2011 +0100
+++ b/ProgTutorial/antiquote_setup.ML	Tue Jun 28 09:22:00 2011 +0100
@@ -98,17 +98,18 @@
 val two_args   = Scan.lift (Args.name -- Args.name)
 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with"  |-- Args.name))
 
-val _ = Thy_Output.antiquotation @{binding "ML"} parser_ml output_ml
-val _ = Thy_Output.antiquotation @{binding "ML_ind"} parser_ml_ind output_ml_ind
-val _ = Thy_Output.antiquotation @{binding "ML_type"} single_arg output_type
-val _ = Thy_Output.antiquotation @{binding "ML_type_ind"} single_arg output_type_ind
-val _ = Thy_Output.antiquotation @{binding "ML_struct"} single_arg output_struct
-val _ = Thy_Output.antiquotation @{binding "ML_struct_ind"} single_arg output_struct_ind
-val _ = Thy_Output.antiquotation @{binding "ML_funct"} single_arg output_funct
-val _ = Thy_Output.antiquotation @{binding "ML_funct_ind"} single_arg output_funct_ind
-val _ = Thy_Output.antiquotation @{binding "ML_response"} two_args output_response
-val _ = Thy_Output.antiquotation @{binding "ML_response_fake"} two_args output_response_fake
-val _ = Thy_Output.antiquotation @{binding "ML_response_fake_both"} two_args ouput_response_fake_both
+val ml_setup = 
+  Thy_Output.antiquotation @{binding "ML"} parser_ml output_ml
+  #> Thy_Output.antiquotation @{binding "ML_ind"} parser_ml_ind output_ml_ind
+  #> Thy_Output.antiquotation @{binding "ML_type"} single_arg output_type
+  #> Thy_Output.antiquotation @{binding "ML_type_ind"} single_arg output_type_ind
+  #> Thy_Output.antiquotation @{binding "ML_struct"} single_arg output_struct
+  #> Thy_Output.antiquotation @{binding "ML_struct_ind"} single_arg output_struct_ind
+  #> Thy_Output.antiquotation @{binding "ML_funct"} single_arg output_funct
+  #> Thy_Output.antiquotation @{binding "ML_funct_ind"} single_arg output_funct_ind
+  #> Thy_Output.antiquotation @{binding "ML_response"} two_args output_response
+  #> Thy_Output.antiquotation @{binding "ML_response_fake"} two_args output_response_fake
+  #> Thy_Output.antiquotation @{binding "ML_response_fake_both"} two_args ouput_response_fake_both
 
 (* FIXME: experimental *)
 fun ml_eq (lhs, pat, eq) =
@@ -120,7 +121,8 @@
      | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e));
      output ctxt ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
 
-val _ = Thy_Output.antiquotation @{binding "ML_response_eq"} test output_response_eq
+val ml_response_setup = 
+  Thy_Output.antiquotation @{binding "ML_response_eq"} test output_response_eq
 
 (* checks whether a file exists in the Isabelle distribution *)
 fun href_link txt =
@@ -136,7 +138,7 @@
    then output ctxt [href_link txt]
    else error (implode ["Source file ", quote txt, " does not exist."]))
 
-val _ = Thy_Output.antiquotation @{binding "ML_file"} single_arg check_file_exists
+val ml_file_setup = Thy_Output.antiquotation @{binding "ML_file"} single_arg check_file_exists
 
 
 (* replaces the official subgoal antiquotation with one *)
@@ -176,7 +178,16 @@
   Thy_Output.output ctxt output
 end
 
-val _ = Thy_Output.antiquotation @{binding "subgoals"} (Scan.succeed ()) output_goals
-val _ = Thy_Output.antiquotation @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state
+val subgoals_setup = 
+  Thy_Output.antiquotation @{binding "subgoals"} (Scan.succeed ()) output_goals
+val raw_goal_state_setup = 
+  Thy_Output.antiquotation @{binding "raw_goal_state"} (Scan.succeed ()) output_raw_goal_state
+
+val setup =
+  ml_setup #>
+  ml_response_setup #>
+  ml_file_setup #>
+  subgoals_setup #>
+  raw_goal_state_setup
 
 end;