# HG changeset patch
# User wenzelm
# Date 878057888 -3600
# Node ID 01745d56307db772cc253263802e55efd43f020f
# Parent  15768dba480ed11e6257ac9721049dc5da858d06
PureThy.add_store_defs_i, PureThy.add_store_axioms_i;

diff -r 15768dba480e -r 01745d56307d src/HOL/typedef.ML
--- a/src/HOL/typedef.ML	Tue Oct 28 17:56:57 1997 +0100
+++ b/src/HOL/typedef.ML	Tue Oct 28 17:58:08 1997 +0100
@@ -114,9 +114,9 @@
      [(name, setT, NoSyn),
       (Rep_name, newT --> oldT, NoSyn),
       (Abs_name, oldT --> newT, NoSyn)]
-    |> Theory.add_defs_i
+    |> PureThy.add_store_defs_i
      [(name ^ "_def", Logic.mk_equals (setC, set))]
-    |> Theory.add_axioms_i
+    |> PureThy.add_store_axioms_i
      [(Rep_name, rep_type),
       (Rep_name ^ "_inverse", rep_type_inv),
       (Abs_name ^ "_inverse", abs_type_inv)]