--- a/ProgTutorial/antiquote_setup.ML	Fri Apr 19 11:09:18 2013 +0100
+++ b/ProgTutorial/antiquote_setup.ML	Fri May 17 11:01:55 2013 +0100
@@ -156,7 +156,7 @@
     | subgoals n = "goal (" ^ string_of_int n ^ " subgoals):"
 
   val state = proof_state node
-  val goals = Goal_Display.pretty_goal {main = false, limit = false} ctxt state
+  val goals = Goal_Display.pretty_goal ctxt state
 
   val {prop, ...} = rep_thm state;
   val (As, _) = Logic.strip_horn prop;