--- a/ProgTutorial/antiquote_setup.ML	Thu Oct 04 13:00:31 2012 +0100
+++ b/ProgTutorial/antiquote_setup.ML	Sat Dec 01 14:51:19 2012 +0000
@@ -144,9 +144,10 @@
 (* replaces the official subgoal antiquotation with one *)
 (* that is closer to the actual output                  *)
 fun proof_state state =
-    (case try Toplevel.proof_of state of
-      SOME prf => prf
-    | _ => error "No proof state")
+  (case try (Proof.goal o Toplevel.proof_of) state of
+    SOME {goal, ...} => goal
+  | _ => error "No proof state");
+
 
 fun output_goals  {state = node, context = ctxt, ...} _ = 
 let
@@ -154,10 +155,10 @@
     | subgoals 1 = "goal (1 subgoal):"
     | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"
 
-  val state = proof_state node;
-  val goals = Pretty.chunks (Proof.pretty_goals false state);
+  val state = proof_state node
+  val goals = Goal_Display.pretty_goal {main = false, limit = false} ctxt state
 
-  val {prop, ...} = (rep_thm o #goal o Proof.goal) state;
+  val {prop, ...} = rep_thm state;
   val (As, _) = Logic.strip_horn prop;
   val output  = (case (length As) of
                       0 => [goals] 
@@ -166,17 +167,14 @@
   Thy_Output.output ctxt output
 end
 
-fun output_raw_goal_state  {state = node, context = ctxt, ...}  _ = 
-let
-  val state = proof_state node;
-  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))
-  val _ = tracing (Pretty.string_of (Pretty.str (Syntax.string_of_term ctxt (prop_of goals))))
-in 
-  Thy_Output.output ctxt output
-end
+fun output_raw_goal_state  {state, context = ctxt, ...}  _ = 
+  let
+    val goals = proof_state state
+    val output  = [Pretty.str (Syntax.string_of_term ctxt (prop_of goals))]  
+  in
+    Thy_Output.output ctxt output
+  end
 
 val subgoals_setup = 
   Thy_Output.antiquotation @{binding "subgoals"} (Scan.succeed ()) output_goals