# HG changeset patch
# User wenzelm
# Date 878208212 -3600
# Node ID 20f7471eedbf094c19d262e6cfd9dbe8d8cf301f
# Parent  0db9f1098fd6ee1fe431fb72e508f2bee642d17e
PureThy.add_store_defs_i, PureThy.add_store_axioms;

diff -r 0db9f1098fd6 -r 20f7471eedbf src/HOL/datatype.ML
--- 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