src/HOL/Nominal/nominal_atoms.ML

     val full_ak_names = map (Sign.intern_type (sign_of thy1)) ak_names;
     val ak_names_types = ak_names ~~ map (Type o rpair []) full_ak_names;
      
     (* adds for every atom-kind an axiom             *)
     (* <ak>_infinite: infinite (UNIV::<ak_type> set) *)
-    val (thy2,inf_axs) = PureThy.add_axioms_i (map (fn (ak_name, T) =>
+    val (inf_axs,thy2) = PureThy.add_axioms_i (map (fn (ak_name, T) =>
       let 
 	val name = ak_name ^ "_infinite"
         val axiom = HOLogic.mk_Trueprop (HOLogic.mk_not
                     (HOLogic.mk_mem (HOLogic.mk_UNIV T,
                      Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T)))))

         end) ak_names_types thy) ak_names_types thy4;
     
     (* proves that every atom-kind is an instance of at *)
     (* lemma at_<ak>_inst:                              *)
     (* at TYPE(<ak>)                                    *)
-    val (thy6, prm_cons_thms) = 
+    val (prm_cons_thms,thy6) = 
       thy5 |> PureThy.add_thms (map (fn (ak_name, T) =>
       let
         val ak_name_qu = Sign.full_name (sign_of thy5) (ak_name);
         val i_type = Type(ak_name_qu,[]);
 	val cat = Const ("nominal.at",(Term.itselfT i_type)  --> HOLogic.boolT);

 
     (* proves that every pt_<ak>-type together with <ak>-type *)
     (* instance of pt                                         *)
     (* lemma pt_<ak>_inst:                                    *)
     (* pt TYPE('x::pt_<ak>) TYPE(<ak>)                        *)
-    val (thy8, prm_inst_thms) = 
+    val (prm_inst_thms,thy8) = 
       thy7 |> PureThy.add_thms (map (fn (ak_name, T) =>
       let
         val ak_name_qu = Sign.full_name (sign_of thy7) (ak_name);
         val pt_name_qu = Sign.full_name (sign_of thy7) ("pt_"^ak_name);
         val i_type1 = TFree("'x",[pt_name_qu]);

 
      (* proves that every fs_<ak>-type together with <ak>-type   *)
      (* instance of fs-type                                      *)
      (* lemma abst_<ak>_inst:                                    *)
      (* fs TYPE('x::pt_<ak>) TYPE (<ak>)                         *)
-     val (thy12, fs_inst_thms) = 
+     val (fs_inst_thms,thy12) = 
        thy11 |> PureThy.add_thms (map (fn (ak_name, T) =>
        let
          val ak_name_qu = Sign.full_name (sign_of thy11) (ak_name);
          val fs_name_qu = Sign.full_name (sign_of thy11) ("fs_"^ak_name);
          val i_type1 = TFree("'x",[fs_name_qu]);

 	   (thy, ak_names_types)) (thy12, ak_names_types)
 
         (* proves for every <ak>-combination a cp_<ak1>_<ak2>_inst theorem;     *)
         (* lemma cp_<ak1>_<ak2>_inst:                                           *)
         (* cp TYPE('a::cp_<ak1>_<ak2>) TYPE(<ak1>) TYPE(<ak2>)                  *)
-        val (thy12c, cp_thms) = foldl_map (fn (thy, (ak_name, T)) =>
-	 foldl_map (fn (thy', (ak_name', T')) =>
+        val (cp_thms,thy12c) = fold_map (fn (ak_name, T) => fn thy =>
+	 fold_map (fn (ak_name', T') => fn thy' =>
            let
              val ak_name_qu  = Sign.full_name (sign_of thy') (ak_name);
 	     val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name');
              val cp_name_qu  = Sign.full_name (sign_of thy') ("cp_"^ak_name^"_"^ak_name');
              val i_type0 = TFree("'a",[cp_name_qu]);

 	     val name = "cp_"^ak_name^ "_"^ak_name'^"_inst";
              val statement = HOLogic.mk_Trueprop (ccp $ cp_type $ at_type $ at_type');
 
              val proof = fn _ => EVERY [auto_tac (claset(),simp_s), rtac cp1 1];
 	   in
-	     thy' |> PureThy.add_thms 
-                    [((name, standard (Goal.prove thy' [] [] statement proof)), [])]
+	     PureThy.add_thms [((name, standard (Goal.prove thy' [] [] statement proof)), [])] thy'
 	   end) 
-	   (thy, ak_names_types)) (thy12b, ak_names_types);
+           ak_names_types thy) ak_names_types thy12b;
        
         (* proves for every non-trivial <ak>-combination a disjointness   *)
         (* theorem; i.e. <ak1> != <ak2>                                   *)
         (* lemma ds_<ak1>_<ak2>:                                          *)
         (* dj TYPE(<ak1>) TYPE(<ak2>)                                     *)
-        val (thy12d, dj_thms) = foldl_map (fn (thy, (ak_name, T)) =>
-	  foldl_map (fn (thy', (ak_name', T')) =>
+        val (dj_thms, thy12d) = fold_map (fn (ak_name,T) => fn thy =>
+	  fold_map (fn (ak_name',T') => fn thy' =>
           (if not (ak_name = ak_name') 
            then 
 	       let
 		 val ak_name_qu  = Sign.full_name (sign_of thy') (ak_name);
 	         val ak_name_qu' = Sign.full_name (sign_of thy') (ak_name');

 	         val name = "dj_"^ak_name^"_"^ak_name';
                  val statement = HOLogic.mk_Trueprop (cdj $ at_type $ at_type');
 
                  val proof = fn _ => auto_tac (claset(),simp_s);
 	       in
-		   thy' |> PureThy.add_thms 
-                        [((name, standard (Goal.prove thy' [] [] statement proof)), []) ]
+		PureThy.add_thms [((name, standard (Goal.prove thy' [] [] statement proof)), [])] thy'
 	       end
            else 
-            (thy',[])))  (* do nothing branch, if ak_name = ak_name' *) 
-	   (thy, ak_names_types)) (thy12c, ak_names_types);
+            ([],thy')))  (* do nothing branch, if ak_name = ak_name' *) 
+	    ak_names_types thy) ak_names_types thy12c;
 
      (*<<<<<<<  pt_<ak> class instances  >>>>>>>*)
      (*=========================================*)
      (* some abbreviations for theorems *)
       val pt1           = thm "pt1";

 
        (* Now we collect and instantiate some lemmas w.r.t. all atom      *)
        (* types; this allows for example to use abs_perm (which is a      *)
        (* collection of theorems) instead of thm abs_fun_pi with explicit *)
        (* instantiations.                                                 *)
-       val (thy33,_) = 
+       val (_,thy33) = 
 	 let 
              (* takes a theorem thm and a list of theorems [t1,..,tn]            *)
              (* produces a list of theorems of the form [t1 RS thm,..,tn RS thm] *) 
              fun instR thm thms = map (fn ti => ti RS thm) thms;
 

                      val i_pt_pt_at_cp_dj = inst_zip djs i_pt_pt_at_cp;
 		 in i_pt_pt_at_cp_dj end;
            in
             thy32 
 	    |>   PureThy.add_thmss [(("alpha", inst_pt_at [abs_fun_eq]),[])]
-            |>>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij]),[])]
-            |>>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])]
-            |>>> PureThy.add_thmss [(("perm_bij", inst_pt_at [pt_bij]),[])]
-            |>>> PureThy.add_thmss [(("perm_compose", inst_pt_at [pt_perm_compose]),[])]
-            |>>> PureThy.add_thmss [(("perm_app_eq", inst_pt_at [perm_eq_app]),[])]
-            |>>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
-            |>>> PureThy.add_thmss [(("fresh_atm", inst_at [at_fresh]),[])]
-            |>>> PureThy.add_thmss [(("calc_atm", inst_at at_calc),[])]
-            |>>> PureThy.add_thmss
+            ||>> PureThy.add_thmss [(("perm_swap", inst_pt_at [pt_swap_bij]),[])]
+            ||>> PureThy.add_thmss [(("perm_fresh_fresh", inst_pt_at [pt_fresh_fresh]),[])]
+            ||>> PureThy.add_thmss [(("perm_bij", inst_pt_at [pt_bij]),[])]
+            ||>> PureThy.add_thmss [(("perm_compose", inst_pt_at [pt_perm_compose]),[])]
+            ||>> PureThy.add_thmss [(("perm_app_eq", inst_pt_at [perm_eq_app]),[])]
+            ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
+            ||>> PureThy.add_thmss [(("fresh_atm", inst_at [at_fresh]),[])]
+            ||>> PureThy.add_thmss [(("calc_atm", inst_at at_calc),[])]
+            ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at [abs_fun_pi]
 		  and thms2 = inst_pt_pt_at_cp [abs_fun_pi_ineq]
 	      in [(("abs_perm", thms1 @ thms2),[])] end
-            |>>> PureThy.add_thmss
+            ||>> PureThy.add_thmss
 	      let val thms1 = inst_dj [dj_perm_forget]
 		  and thms2 = inst_dj [dj_pp_forget]
               in [(("perm_dj", thms1 @ thms2),[])] end
-            |>>> PureThy.add_thmss
+            ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at_fs [fresh_iff]
 		  and thms2 = inst_pt_pt_at_cp_dj [fresh_iff_ineq]
 	    in [(("abs_fresh", thms1 @ thms2),[])] end
-	    |>>> PureThy.add_thmss
+	    ||>> PureThy.add_thmss
 	      let val thms1 = inst_pt_at [abs_fun_supp]
 		  and thms2 = inst_pt_at_fs [abs_fun_supp]
 		  and thms3 = inst_pt_pt_at_cp_dj [abs_fun_supp_ineq]
 	      in [(("abs_supp", thms1 @ thms2 @ thms3),[])] end
 	   end;