--- a/ProgTutorial/antiquote_setup.ML	Fri Oct 30 09:42:17 2009 +0100
+++ b/ProgTutorial/antiquote_setup.ML	Fri Oct 30 09:42:17 2009 +0100
@@ -155,7 +155,7 @@
   val state = proof_state node;
   val goals = Pretty.chunks (Proof.pretty_goals false state);
 
-  val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd);
+  val {prop, ...} = (rep_thm o #goal o Proof.goal) state;
   val (As, _) = Logic.strip_horn prop;
   val output  = (case (length As) of
                       0 => [goals] 
@@ -167,7 +167,7 @@
 fun output_raw_goal_state  {state = node, context = ctxt, ...}  _ = 
 let
   val state = proof_state node;
-  val goals = (Proof.get_goal state |> snd |> snd)
+  val goals = (#goal o Proof.goal) state;
 
   val output  = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))]  
   val _ = tracing (Syntax.string_of_term ctxt (prop_of goals))