Adapted to new type of store_thmss(_atts).

--- a/src/HOL/Nominal/nominal_package.ML	Mon Dec 05 00:38:07 2005 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Mon Dec 05 00:39:18 2005 +0100
@@ -1067,25 +1067,25 @@
 
     val simp_atts = replicate (length new_type_names) [Simplifier.simp_add_global];
 
-    val (thy9, _) = thy8 |>
+    val (_, thy9) = thy8 |>
       Theory.add_path big_name |>
-      PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] |>>
-      Theory.parent_path |>>>
-      DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms |>>>
-      DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss |>>>
-      DatatypeAux.store_thmss_atts "perm" new_type_names simp_atts perm_simps' |>>>
-      DatatypeAux.store_thmss "inject" new_type_names inject_thms |>>>
-      DatatypeAux.store_thmss "supp" new_type_names supp_thms |>>>
-      DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms |>>
+      (PureThy.add_thms [(("induct_weak", dt_induct), [case_names_induct])] #> Library.swap) ||>
+      Theory.parent_path ||>>
+      DatatypeAux.store_thmss_atts "distinct" new_type_names simp_atts distinct_thms ||>>
+      DatatypeAux.store_thmss "constr_rep" new_type_names constr_rep_thmss ||>>
+      DatatypeAux.store_thmss_atts "perm" new_type_names simp_atts perm_simps' ||>>
+      DatatypeAux.store_thmss "inject" new_type_names inject_thms ||>>
+      DatatypeAux.store_thmss "supp" new_type_names supp_thms ||>>
+      DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms ||>
       fold (fn (atom, ths) => fn thy =>
         let val class = Sign.intern_class thy ("fs_" ^ Sign.base_name atom)
         in fold (fn T => AxClass.add_inst_arity_i
             (fst (dest_Type T),
               replicate (length sorts) [class], [class])
             (AxClass.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
-        end) (atoms ~~ finite_supp_thms) |>>
-      Theory.add_path big_name |>>>
-      PureThy.add_axioms_i [(("induct_unsafe", induct), [case_names_induct])] |>>
+        end) (atoms ~~ finite_supp_thms) ||>
+      Theory.add_path big_name ||>>
+      (PureThy.add_axioms_i [(("induct_unsafe", induct), [case_names_induct])] #> Library.swap) ||>
       Theory.parent_path;
 
   in