--- a/ProgTutorial/antiquote_setup.ML	Wed Jun 02 10:08:16 2010 +0200
+++ b/ProgTutorial/antiquote_setup.ML	Tue Jun 08 15:18:30 2010 +0200
@@ -33,7 +33,7 @@
 
 (* eval function *)
 fun eval_fn ctxt exp =
-  ML_Context.eval_in (SOME ctxt) false Position.none exp
+  ML_Context.eval_text_in (SOME ctxt) false Position.none exp
 
 (* checks and prints a possibly open expressions, no index *)
 fun output_ml {context = ctxt, ...} (txt, (vs, stru)) =
@@ -98,17 +98,17 @@
 val two_args   = Scan.lift (Args.name -- Args.name)
 val test = Scan.lift (Args.name -- Args.name -- Scan.option (Args.$$$ "with"  |-- Args.name))
 
-val _ = ThyOutput.antiquotation "ML" parser_ml output_ml
-val _ = ThyOutput.antiquotation "ML_ind" parser_ml_ind output_ml_ind
-val _ = ThyOutput.antiquotation "ML_type" single_arg output_type
-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
+val _ = Thy_Output.antiquotation "ML" parser_ml output_ml
+val _ = Thy_Output.antiquotation "ML_ind" parser_ml_ind output_ml_ind
+val _ = Thy_Output.antiquotation "ML_type" single_arg output_type
+val _ = Thy_Output.antiquotation "ML_type_ind" single_arg output_type_ind
+val _ = Thy_Output.antiquotation "ML_struct" single_arg output_struct
+val _ = Thy_Output.antiquotation "ML_struct_ind" single_arg output_struct_ind
+val _ = Thy_Output.antiquotation "ML_funct" single_arg output_funct
+val _ = Thy_Output.antiquotation "ML_funct_ind" single_arg output_funct_ind
+val _ = Thy_Output.antiquotation "ML_response" two_args output_response
+val _ = Thy_Output.antiquotation "ML_response_fake" two_args output_response_fake
+val _ = Thy_Output.antiquotation "ML_response_fake_both" two_args ouput_response_fake_both
 
 (* FIXME: experimental *)
 fun ml_eq (lhs, pat, eq) =
@@ -120,7 +120,7 @@
      | SOME e => eval_fn ctxt (ml_eq (lhs, pat, e));
      output ((prefix_lines "" lhs) @ (prefix_lines "> " pat)))
 
-val _ = ThyOutput.antiquotation "ML_response_eq" test output_response_eq
+val _ = Thy_Output.antiquotation "ML_response_eq" test output_response_eq
 
 (* checks whether a file exists in the Isabelle distribution *)
 fun href_link txt =
@@ -136,7 +136,7 @@
    then output [href_link txt]
    else error (implode ["Source file ", quote txt, " does not exist."]))
 
-val _ = ThyOutput.antiquotation "ML_file" single_arg check_file_exists
+val _ = Thy_Output.antiquotation "ML_file" single_arg check_file_exists
 
 
 (* replaces the official subgoal antiquotation with one *)
@@ -161,7 +161,7 @@
                       0 => [goals] 
                     | n => [Pretty.str (subgoals n), goals])  
 in 
-  ThyOutput.output output
+  Thy_Output.output output
 end
 
 fun output_raw_goal_state  {state = node, context = ctxt, ...}  _ = 
@@ -173,10 +173,10 @@
   val _ = tracing (Syntax.string_of_term ctxt (prop_of goals))
   val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals))))
 in 
-  ThyOutput.output output
+  Thy_Output.output output
 end
 
-val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals
-val _ = ThyOutput.antiquotation "raw_goal_state" (Scan.succeed ()) output_raw_goal_state
+val _ = Thy_Output.antiquotation "subgoals" (Scan.succeed ()) output_goals
+val _ = Thy_Output.antiquotation "raw_goal_state" (Scan.succeed ()) output_raw_goal_state
 
 end;