diff -r 6ea1062da89a -r ac3309722536 thys/UF.thy
--- a/thys/UF.thy	Mon Apr 22 10:33:40 2013 +0100
+++ b/thys/UF.thy	Wed Apr 24 09:49:00 2013 +0100
@@ -533,10 +533,9 @@
   where
   "rec_Minr rf = 
      (let vl = arity rf
-      in let rq = rec_all (id vl (vl - 1)) (Cn (Suc vl) 
-              rec_not [Cn (Suc vl) rf 
-                    (get_fstn_args (Suc vl) (vl - 1) @
-                                        [id (Suc vl) (vl)])]) 
+      in let rq = rec_all (id vl (vl - 1)) 
+                  (Cn (Suc vl) rec_not [Cn (Suc vl) rf 
+                    (get_fstn_args (Suc vl) (vl - 1) @ [id (Suc vl) vl])]) 
       in  rec_sigma rq)"
 
 lemma length_getpren_params[simp]: "length (get_fstn_args m n) = n"
@@ -766,13 +765,12 @@
   "rec_maxr rr = (let vl = arity rr in 
                   let rt = id (Suc vl) (vl - 1) in
                   let rf1 = Cn (Suc (Suc vl)) rec_le 
-                    [id (Suc (Suc vl)) 
-                     ((Suc vl)), id (Suc (Suc vl)) (vl)] in
+                    [id (Suc (Suc vl)) (Suc vl), id (Suc (Suc vl)) vl] in
                   let rf2 = Cn (Suc (Suc vl)) rec_not 
                       [Cn (Suc (Suc vl)) 
                            rr (get_fstn_args (Suc (Suc vl)) 
                             (vl - 1) @ 
-                             [id (Suc (Suc vl)) ((Suc vl))])] in
+                             [id (Suc (Suc vl)) (Suc vl)])] in
                   let rf = Cn (Suc (Suc vl)) rec_disj [rf1, rf2] in
                   let Qf = Cn (Suc vl) rec_not [rec_all rt rf]
                   in Cn vl (rec_sigma Qf) (get_fstn_args vl vl @
@@ -1948,10 +1946,8 @@
   where
   "rec_lg = 
   (let rec_lgR = Cn 3 rec_le [Cn 3 rec_power [id 3 1, id 3 2], id 3 0] in
-   let conR1 = Cn 2 rec_conj [Cn 2 rec_less 
-                     [Cn 2 (constn 1) [id 2 0], id 2 0], 
-                            Cn 2 rec_less [Cn 2 (constn 1) 
-                                 [id 2 0], id 2 1]] in 
+   let conR1 = Cn 2 rec_conj [Cn 2 rec_less [Cn 2 (constn 1) [id 2 0], id 2 0], 
+                              Cn 2 rec_less [Cn 2 (constn 1) [id 2 0], id 2 1]] in 
    let conR2 = Cn 2 rec_not [conR1] in 
       Cn 2 rec_add [Cn 2 rec_mult [conR1, Cn 2 (rec_maxr rec_lgR)
                                                [id 2 0, id 2 1, id 2 0]],