# HG changeset patch
# User wenzelm
# Date 878057817 -3600
# Node ID 15768dba480ed11e6257ac9721049dc5da858d06
# Parent  b94dc94be4b7e307a791d57098ad094cfa15f06a
PureThy.add_store_defs_i;

diff -r b94dc94be4b7 -r 15768dba480e TFL/tfl.sml
--- a/TFL/tfl.sml	Tue Oct 28 17:56:15 1997 +0100
+++ b/TFL/tfl.sml	Tue Oct 28 17:56:57 1997 +0100
@@ -338,7 +338,7 @@
 	 Sign.infer_types (sign_of thy) (K None) (K None) [] false
 	       ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], 
 		propT)
-  in  Theory.add_defs_i [(def_name, def_term)] thy  end
+  in  PureThy.add_store_defs_i [(def_name, def_term)] thy  end
 end;
 
 
@@ -458,7 +458,7 @@
      val full_rqt = WFR::TCs
      val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
      val R'abs = S.rand R'
-     val theory = Theory.add_defs_i [(Name ^ "_def", subst_free[(R1,R')] proto_def)]
+     val theory = PureThy.add_store_defs_i [(Name ^ "_def", subst_free[(R1,R')] proto_def)]
 	                     thy
      val def = freezeT((get_axiom theory (Name ^ "_def")) RS meta_eq_to_obj_eq)
      val fconst = #lhs(S.dest_eq(concl def)) 
diff -r b94dc94be4b7 -r 15768dba480e src/HOL/add_ind_def.ML
--- a/src/HOL/add_ind_def.ML	Tue Oct 28 17:56:15 1997 +0100
+++ b/src/HOL/add_ind_def.ML	Tue Oct 28 17:56:57 1997 +0100
@@ -159,7 +159,7 @@
              | x::_ => error ("Illegal occurrence of recursion op: " ^ x ^
                                "\n\t*Consider adding type constraints*"))
 
-  in  thy |> Theory.add_defs_i axpairs  end
+  in  thy |> PureThy.add_store_defs_i axpairs  end
 
 
 end;
diff -r b94dc94be4b7 -r 15768dba480e src/ZF/add_ind_def.ML
--- a/src/ZF/add_ind_def.ML	Tue Oct 28 17:56:15 1997 +0100
+++ b/src/ZF/add_ind_def.ML	Tue Oct 28 17:56:57 1997 +0100
@@ -164,7 +164,7 @@
 
     val dummy = seq (writeln o Sign.string_of_term sign o #2) axpairs
   
-  in  thy |> Theory.add_defs_i axpairs  end
+  in  thy |> PureThy.add_store_defs_i axpairs  end
 
 
 (*Expects the recursive sets to have been defined already.
@@ -257,7 +257,7 @@
   in
     thy
     |> Theory.add_consts_i const_decs
-    |> Theory.add_defs_i axpairs
+    |> PureThy.add_store_defs_i axpairs
   end;