diff -r fea1b7ce5c4a -r 25371f74c768 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Mon Oct 17 13:30:49 2011 +0100
+++ b/ProgTutorial/Tactical.thy	Wed Oct 26 12:59:44 2011 +0100
@@ -13,6 +13,13 @@
 chapter {* Tactical Reasoning\label{chp:tactical} *}
 
 text {*
+   \begin{flushright}
+  {\em ``The most effective debugging tool is still careful thought, coupled with 
+  judiciously placed print statements.''} \\[1ex]
+  Brian Kernighan 
+  \end{flushright}
+
+  \medskip
   One of the main reason for descending to the ML-level of Isabelle is to be
   able to implement automatic proof procedures. Such proof procedures can
   considerably lessen the burden of manual reasoning. They are centred around
@@ -1581,7 +1588,7 @@
 \begin{figure}[p]
 \begin{boxedminipage}{\textwidth}
 \begin{isabelle} *}
-types  prm = "(nat \<times> nat) list"
+type_synonym  prm = "(nat \<times> nat) list"
 consts perm :: "prm \<Rightarrow> 'a \<Rightarrow> 'a"  ("_ \<bullet> _" [80,80] 80)
 
 overloading 
@@ -2472,7 +2479,7 @@
   val xs = strip_abs_vars (term_of rhs)
   val (_, ctxt') = Variable.add_fixes (map fst xs) ctxt
   
-  val thy = ProofContext.theory_of ctxt'
+  val thy = Proof_Context.theory_of ctxt'
   val cxs = map (cterm_of thy o Free) xs
   val new_lhs = Drule.list_comb (lhs, cxs)
 
@@ -2480,7 +2487,7 @@
     | get_conv (_::xs) = Conv.fun_conv (get_conv xs)
 in
   get_conv xs new_lhs |>  
-  singleton (ProofContext.export ctxt' ctxt)
+  singleton (Proof_Context.export ctxt' ctxt)
 end*}
 
 text {*