PureThy.add_store_defs_i, PureThy.add_store_axioms;

--- a/src/HOL/datatype.ML	Thu Oct 30 11:19:57 1997 +0100
+++ b/src/HOL/datatype.ML	Thu Oct 30 11:43:32 1997 +0100
@@ -524,14 +524,14 @@
           val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair;
           val varT = Type.varifyT T;
           val ftyp = the (Sign.const_type sg (Sign.intern_const sg fname));
-        in Theory.add_defs_i [defpairT] thy end;
+        in PureThy.add_store_defs_i [defpairT] thy end;
 
     in
       (thy |> Theory.add_types types
            |> Theory.add_arities arities
            |> Theory.add_consts consts
            |> Theory.add_trrules xrules
-           |> Theory.add_axioms rules, add_primrec, size_eqns, split_eqn)
+           |> PureThy.add_store_axioms rules, add_primrec, size_eqns, split_eqn)
     end
 
 (*Warn if the (induction) variable occurs Free among the premises, which