--- a/ProgTutorial/antiquote_setup.ML	Tue Mar 24 18:06:20 2009 +0100
+++ b/ProgTutorial/antiquote_setup.ML	Wed Mar 25 15:09:04 2009 +0100
@@ -111,18 +111,17 @@
     | _ => error "No proof state")
 
   val state = proof_state node;
-  val goals = Proof.pretty_goals false state;
+  val goals = Pretty.chunks (Proof.pretty_goals false state);
 
   val {prop, ...} = rep_thm (Proof.get_goal state |> snd |> snd);
   val (As, B) = Logic.strip_horn prop;
   val output  = (case (length As) of
-                      0 => goals 
-                    | n => (Pretty.str (subgoals n))::goals)  
+                      0 => [goals] 
+                    | n => [Pretty.str (subgoals n), goals])  
 in 
   ThyOutput.output output
 end
 
-
 val _ = ThyOutput.antiquotation "subgoals" (Scan.succeed ()) output_goals
-   
+ 
 end;