# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1368784915 -3600
# Node ID 4a1539a2c18ef19f88a82afd111cb89dbaa89f17
# Parent  501491d56798653d9c93e84f39e83c12fcac17db
updated to new Isabelle

diff -r 501491d56798 -r 4a1539a2c18e ProgTutorial/antiquote_setup.ML
--- 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;
diff -r 501491d56798 -r 4a1539a2c18e progtutorial.pdf
Binary file progtutorial.pdf has changed