diff -r d144fc51fe04 -r 96d10631eec2 ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Sat Dec 01 16:50:46 2012 +0000
+++ b/ProgTutorial/Tactical.thy	Mon Dec 31 20:20:55 2012 +0000
@@ -524,7 +524,11 @@
 ML %grayML{*fun foc_tac {prems, params, asms, concl, context, schematics} = 
 let 
   fun assgn1 f1 f2 xs =
-    Pretty.list "" "" (map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs) 
+    let
+      val out = map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs
+    in
+      Pretty.list "" "" out
+    end 
 
   fun assgn2 f xs = assgn1 f f xs 
  
@@ -558,10 +562,10 @@
   \begin{quote}\small
   \begin{tabular}{ll}
   params:      & @{text "x:= x"}, @{text "y:= y"}\\
-  schematics:  & @{text "?z:=z"}\\
   assumptions: & @{term "A x y"}\\
   conclusion:  & @{term "B y x \<longrightarrow> C (z y) x"}\\
-  premises:    & @{term "A x y"}
+  premises:    & @{term "A x y"}\\
+  schematics:  & @{text "?z:=z"}
   \end{tabular}
   \end{quote}
 
@@ -586,10 +590,10 @@
   \begin{quote}\small
   \begin{tabular}{ll}
   params:      & @{text "x:= x"}, @{text "y:= y"}\\
-  schematics:  & @{text "?z:=z"}\\
   assumptions: & @{term "A x y"}, @{term "B y x"}\\
   conclusion:  & @{term "C (z y) x"}\\
-  premises:    & @{term "A x y"}, @{term "B y x"}
+  premises:    & @{term "A x y"}, @{term "B y x"}\\
+  schematics:  & @{text "?z:=z"}
   \end{tabular}
   \end{quote}
 *}