adapted to new PureThy.add_thms etc.;

--- a/src/HOL/Tools/record_package.ML	Mon Mar 13 13:16:43 2000 +0100
+++ b/src/HOL/Tools/record_package.ML	Mon Mar 13 13:16:57 2000 +0100
@@ -56,8 +56,6 @@
 val (op :==) = Logic.mk_defpair;
 val (op ===) = HOLogic.mk_Trueprop o HOLogic.mk_eq;
 
-fun get_defs thy specs = map (PureThy.get_thm thy o fst) specs;
-
 
 (* proof by simplification *)
 
@@ -613,15 +611,11 @@
 
     (* 2nd stage: defs_thy *)
 
-    val defs_thy =
+    val (defs_thy, (field_defs, dest_defs)) =
       types_thy
-       |> (Theory.add_consts_i o map (Syntax.no_syn o apfst base))
-         (field_decls @ dest_decls)
-       |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal])))
-         (field_specs @ dest_specs);
-
-    val field_defs = get_defs defs_thy field_specs;
-    val dest_defs = get_defs defs_thy dest_specs;
+       |> (Theory.add_consts_i o map (Syntax.no_syn o apfst base)) (field_decls @ dest_decls)
+       |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) field_specs
+       |>>> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) dest_specs;
 
 
     (* 3rd stage: thms_thy *)
@@ -639,7 +633,7 @@
 
     val thms_thy =
       defs_thy
-      |> (PureThy.add_thmss o map Thm.no_attributes)
+      |> (#1 oo (PureThy.add_thmss o map Thm.no_attributes))
         [("field_defs", field_defs),
           ("dest_defs", dest_defs),
           ("dest_convs", dest_convs),
@@ -782,7 +776,7 @@
 
     (* 2nd stage: defs_thy *)
 
-    val defs_thy =
+    val (defs_thy, ((sel_defs, update_defs), make_defs)) =
       fields_thy
       |> Theory.parent_path
       |> Theory.add_tyabbrs_i recordT_specs     (*not made part of record name space!*)
@@ -790,13 +784,9 @@
       |> Theory.add_trfuns ([], [], field_tr's, [])
       |> (Theory.add_consts_i o map Syntax.no_syn)
         (sel_decls @ update_decls @ make_decls)
-      |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal])))
-        (sel_specs @ update_specs)
-      |> (PureThy.add_defs_i o map Thm.no_attributes) make_specs;
-
-    val sel_defs = get_defs defs_thy sel_specs;
-    val update_defs = get_defs defs_thy update_specs;
-    val make_defs = get_defs defs_thy make_specs;
+      |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) sel_specs
+      |>>> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) update_specs
+      |>>> (PureThy.add_defs_i o map Thm.no_attributes) make_specs;
 
 
     (* 3rd stage: thms_thy *)
@@ -812,13 +802,13 @@
 
     val thms_thy =
       defs_thy
-      |> (PureThy.add_thmss o map Thm.no_attributes)
+      |> (#1 oo (PureThy.add_thmss o map Thm.no_attributes))
         [("select_defs", sel_defs),
           ("update_defs", update_defs),
           ("make_defs", make_defs),
           ("select_convs", sel_convs),
           ("update_convs", update_convs)]
-      |> PureThy.add_thmss
+      |> (#1 oo PureThy.add_thmss)
         [(("simps", simps), [Simplifier.simp_add_global]),
          (("iffs", iffs), [iff_add_global])];
 

--- a/src/HOL/Tools/typedef_package.ML	Mon Mar 13 13:16:43 2000 +0100
+++ b/src/HOL/Tools/typedef_package.ML	Mon Mar 13 13:16:57 2000 +0100
@@ -140,9 +140,9 @@
        ((if no_def then [] else [(name, setT, NoSyn)]) @
         [(Rep_name, newT --> oldT, NoSyn),
          (Abs_name, oldT --> newT, NoSyn)])
-      |> (if no_def then I else (PureThy.add_defs_i o map Thm.no_attributes)
+      |> (if no_def then I else (#1 oo (PureThy.add_defs_i o map Thm.no_attributes))
        [Logic.mk_defpair (setC, set)])
-      |> (PureThy.add_axioms_i o map Thm.no_attributes)
+      |> (#1 oo (PureThy.add_axioms_i o map Thm.no_attributes))
        [(Rep_name, rep_type),
         (Rep_name ^ "_inverse", rep_type_inv),
         (Abs_name ^ "_inverse", abs_type_inv)]

--- a/src/Pure/Isar/isar_thy.ML	Mon Mar 13 13:16:43 2000 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Mon Mar 13 13:16:57 2000 +0100
@@ -216,10 +216,10 @@
 fun add_axms f args thy =
   f (map (fn (x, srcs) => (x, map (Attrib.global_attribute thy) srcs)) args) thy;
 
-val add_axioms = add_axms PureThy.add_axioms o map Comment.ignore;
-val add_axioms_i = PureThy.add_axioms_i o map Comment.ignore;
-val add_defs = add_axms PureThy.add_defs o map Comment.ignore;
-val add_defs_i = PureThy.add_defs_i o map Comment.ignore;
+val add_axioms = add_axms (#1 oo PureThy.add_axioms) o map Comment.ignore;
+val add_axioms_i = (#1 oo PureThy.add_axioms_i) o map Comment.ignore;
+val add_defs = add_axms (#1 oo PureThy.add_defs) o map Comment.ignore;
+val add_defs_i = (#1 oo PureThy.add_defs_i) o map Comment.ignore;
 
 
 (* constdefs *)