diff -r ccec33db31d4 -r 4457185b22ef thys2/Translation2.thy
--- a/thys2/Translation2.thy	Wed Jun 26 14:42:42 2013 +0100
+++ b/thys2/Translation2.thy	Wed Jul 17 10:33:19 2013 +0100
@@ -51,20 +51,30 @@
   "rec_ci (Cn n f gs) = (let cied_gs = map (\<lambda> g. rec_ci g) gs in
                        let cied_f = rec_ci f in 
                        let qstr = Max (set (map snd (cied_f # cied_gs))) in 
-                       (cn_merge_gs cied_gs n qstr; mv_boxes 0 (qstr + length gs) n; 
-                         mv_boxes qstr 0 (length gs) ; fst cied_f; mv_box (arity f) (Suc (qstr + length gs)); 
-                         empty_boxes (length gs); mv_boxes (qstr + length gs) 0 (Suc n),  Suc (qstr + length gs + n)))" |
+                       (cn_merge_gs cied_gs n qstr; 
+                        mv_boxes 0 (qstr + length gs) n; 
+                        mv_boxes qstr 0 (length gs) ; 
+                        fst cied_f; 
+                        mv_box (arity f) (Suc (qstr + length gs)); 
+                        empty_boxes (length gs); 
+                        mv_boxes (qstr + length gs) 0 (Suc n),  Suc (qstr + length gs + n)))" |
   "rec_ci (Pr n f g) = (let (fa, fp) = rec_ci f in 
                          let (ga, gp) = rec_ci g in 
                          let qstr = max fp gp in 
                          let e = length ga + 7 in 
-                         (mv_box 0 qstr; mv_boxes 1 0 n; fa; mv_box n (Suc qstr); mv_boxes 0 2 n;
-                          mv_box (Suc qstr) 1; (([Dec qstr e] ; ga ; [Inc 0, Dec (Suc n) 3, Goto 1]) @ 
-                          [Dec (Suc (Suc n)) 0, Inc 1, Goto (length ga + 4)]), Suc qstr))" |
+                         (mv_box 0 qstr; 
+                          mv_boxes 1 0 n; 
+                          fa; 
+                          mv_box n (Suc qstr); 
+                          mv_boxes 0 2 n;
+                          mv_box (Suc qstr) 1; 
+                          (([Dec qstr e] ; ga ; [Inc 0, Dec (Suc n) 3, Goto 1]) @ 
+                            [Dec (Suc (Suc n)) 0, Inc 1, Goto (length ga + 4)]), Suc qstr))" |
   "rec_ci (Mn n f) = (let (fa, fp) = rec_ci f in
                       let len = length fa in  
-                      (mv_boxes 0 (Suc 0) n; (fa @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3),
-                       Goto (len + 1), Inc 0, Goto 0]), fp))"
+                      (mv_boxes 0 (Suc 0) n; 
+                       (fa @ [Dec (Suc n) (len + 5), Dec (Suc n) (len + 3),
+                              Goto (len + 1), Inc 0, Goto 0]), fp))"