--- a/ProgTutorial/Advanced.thy	Thu Oct 04 13:00:31 2012 +0100
+++ b/ProgTutorial/Advanced.thy	Sat Dec 01 14:51:19 2012 +0000
@@ -8,7 +8,12 @@
 text {*
    \begin{flushright}
   {\em All things are difficult before they are easy.} \\[1ex]
-  proverb
+  proverb\\[2ex]
+  {\em Programming is not just an act of telling a computer what 
+  to do: it is also an act of telling other programmers what you 
+  wished the computer to do. Both are important, and the latter 
+  deserves care.}\\[1ex]
+  ---Andrew Morton, Linux Kernel mailinglist, 13 March 2012
   \end{flushright}
 
   \medskip

--- a/ProgTutorial/Package/Ind_Extensions.thy	Thu Oct 04 13:00:31 2012 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Sat Dec 01 14:51:19 2012 +0000
@@ -192,7 +192,7 @@
 
 text {* Type declarations *}
 
-ML %grayML{*Typedef.add_typedef_global false NONE (@{binding test},[],NoSyn)
+ML %grayML{*Typedef.add_typedef_global (@{binding test}, [], NoSyn)
   @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *}
 
 ML %grayML{*fun pat_completeness_auto ctxt =

--- a/ProgTutorial/Parsing.thy	Thu Oct 04 13:00:31 2012 +0100
+++ b/ProgTutorial/Parsing.thy	Sat Dec 01 14:51:19 2012 +0000
@@ -9,7 +9,7 @@
   \begin{flushright}
   {\em An important principle underlying the success and popularity of Unix\\ is
   the philosophy of building on the work of others.} \\[1ex]
-  Linus Torwalds in the email exchange\\ with Andrew S.~Tannenbaum
+  Tony Travis in an email about the\\ ``LINUX is obsolete'' debate 
   \end{flushright}
 
 

--- 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

Binary file progtutorial.pdf has changed