src/HOL/Nominal/nominal_package.ML

       else map (fn T => Sign.intern_class thy8 ("fs_" ^
         Sign.base_name (fst (dest_Type T)))) dt_atomTs;
     val fsT = TFree ("'n", ind_sort);
 
     fun make_pred i T =
-      Free (List.nth (pnames, i), T --> fsT --> HOLogic.boolT);
+      Free (List.nth (pnames, i), fsT --> T --> HOLogic.boolT);
 
     fun make_ind_prem k T ((cname, cargs), idxs) =
       let
         val recs = List.filter is_rec_type cargs;
         val Ts = map (typ_of_dtyp descr'' sorts') cargs;

         fun mk_prem ((dt, s), T) =
           let
             val (Us, U) = strip_type T;
             val l = length Us
           in list_all (z :: map (pair "x") Us, HOLogic.mk_Trueprop
-            (make_pred (body_index dt) U $ app_bnds (Free (s, T)) l $ Bound l))
+            (make_pred (body_index dt) U $ Bound l $ app_bnds (Free (s, T)) l))
           end;
 
         val prems = map mk_prem (recs ~~ rec_tnames ~~ recTs');
         val prems' = map (fn p as (_, T) => HOLogic.mk_Trueprop
             (Const ("nominal.fresh", T --> fsT --> HOLogic.boolT) $
               Free p $ Free z))
           (map (curry List.nth frees) (List.concat (map (fn (m, n) =>
              m upto m + n - 1) idxs)))
 
-      in list_all_free (z :: frees, Logic.list_implies (prems' @ prems,
-        HOLogic.mk_Trueprop (make_pred k T $ 
-          list_comb (Const (cname, Ts ---> T), map Free frees) $ Free z)))
+      in list_all_free (frees @ [z], Logic.list_implies (prems' @ prems,
+        HOLogic.mk_Trueprop (make_pred k T $ Free z $
+          list_comb (Const (cname, Ts ---> T), map Free frees))))
       end;
 
     val ind_prems = List.concat (map (fn (((i, (_, _, constrs)), (_, idxss)), T) =>
       map (make_ind_prem i T) (constrs ~~ idxss)) (descr'' ~~ ndescr ~~ recTs));
     val tnames = DatatypeProp.make_tnames recTs;
     val z = (variant tnames "z", fsT);
     val ind_concl = HOLogic.mk_Trueprop (foldr1 (HOLogic.mk_binop "op &")
-      (map (fn (((i, _), T), tname) => make_pred i T $ Free (tname, T) $ Free z)
+      (map (fn (((i, _), T), tname) => make_pred i T $ Free z $ Free (tname, T))
         (descr'' ~~ recTs ~~ tnames)));
     val induct = Logic.list_implies (ind_prems, ind_concl);
 
     val simp_atts = replicate (length new_type_names) [Simplifier.simp_add_global];