Adapted to new type of PureThy.add_defs_i.

--- a/src/HOL/Nominal/nominal_atoms.ML	Wed Dec 07 16:47:04 2005 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Dec 08 10:17:21 2005 +0100
@@ -89,7 +89,7 @@
         val def2 = Logic.mk_equals (cswap $ ab $ c, cswap_akname $ ab $ c)
       in
         thy |> Theory.add_consts_i [("swap_" ^ ak_name, swapT, NoSyn)] 
-            |> (#1 o PureThy.add_defs_i true [((name, def2),[])])
+            |> (#2 o PureThy.add_defs_i true [((name, def2),[])])
             |> PrimrecPackage.add_primrec_i "" [(("", def1),[])]            
       end) (thy2, ak_names_types);
     
@@ -130,8 +130,8 @@
     (*                                                                   *)
     (* the trivial cases are added to the simplifier, while the non-     *)
     (* have their own rules proved below                                 *)  
-    val (thy5, perm_defs) = foldl_map (fn (thy, (ak_name, T)) =>
-      foldl_map (fn (thy', (ak_name', T')) =>
+    val (perm_defs, thy5) = fold_map (fn (ak_name, T) => fn thy =>
+      fold_map (fn (ak_name', T') => fn thy' =>
         let
           val perm_def_name = ak_name ^ "_prm_" ^ ak_name';
           val pi = Free ("pi", mk_permT T);
@@ -143,8 +143,8 @@
           val def = Logic.mk_equals
                     (cperm $ pi $ a, if ak_name = ak_name' then cperm_def $ pi $ a else a)
         in
-          thy' |> PureThy.add_defs_i true [((name, def),[])] 
-        end) (thy, ak_names_types)) (thy4, ak_names_types);
+          PureThy.add_defs_i true [((name, def),[])] thy'
+        end) ak_names_types thy) ak_names_types thy4;
     
     (* proves that every atom-kind is an instance of at *)
     (* lemma at_<ak>_inst:                              *)

--- a/src/HOL/Nominal/nominal_package.ML	Wed Dec 07 16:47:04 2005 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Thu Dec 08 10:17:21 2005 +0100
@@ -489,8 +489,8 @@
 
     val _ = warning "defining type...";
 
-    val (thy6, typedefs) =
-      foldl_map (fn (thy, ((((name, mx), tvs), c), name')) =>
+    val (typedefs, thy6) =
+      fold_map (fn ((((name, mx), tvs), c), name') => fn thy =>
         setmp TypedefPackage.quiet_mode true
           (TypedefPackage.add_typedef_i false (SOME name') (name, tvs, mx) c NONE
             (rtac exI 1 THEN
@@ -502,7 +502,7 @@
           val tvs' = map (fn s => TFree (s, the (AList.lookup op = sorts' s))) tvs;
           val T = Type (Sign.intern_type thy name, tvs');
           val Const (_, Type (_, [U])) = c
-        in apsnd (pair r o hd)
+        in apfst (pair r o hd)
           (PureThy.add_defs_i true [(("prm_" ^ name ^ "_def", Logic.mk_equals
             (Const ("nominal.perm", permT --> T --> T) $ pi $ Free ("x", T),
              Const (Sign.intern_const thy ("Abs_" ^ name), U --> T) $
@@ -510,8 +510,8 @@
                  (Const (Sign.intern_const thy ("Rep_" ^ name), T --> U) $
                    Free ("x", T))))), [])] thy)
         end))
-          (thy5, types_syntax ~~ tyvars ~~
-            (List.take (ind_consts, length new_type_names)) ~~ new_type_names);
+          (types_syntax ~~ tyvars ~~
+            (List.take (ind_consts, length new_type_names)) ~~ new_type_names) thy5;
 
     val perm_defs = map snd typedefs;
     val Abs_inverse_thms = map (#Abs_inverse o fst) typedefs;
@@ -667,7 +667,7 @@
         val eqn = HOLogic.mk_Trueprop (HOLogic.mk_eq
           (Const (rep_name, T --> T') $ lhs, rhs));
         val def_name = (Sign.base_name cname) ^ "_def";
-        val (thy', [def_thm]) = thy |>
+        val ([def_thm], thy') = thy |>
           Theory.add_consts_i [(cname', constrT, mx)] |>
           (PureThy.add_defs_i false o map Thm.no_attributes) [(def_name, def)]
       in (thy', defs @ [def_thm], eqns @ [eqn]) end;