# HG changeset patch
# User wenzelm
# Date 893842407 -7200
# Node ID cf554f1c65be4cdc723fefd8c76e552f95c929e0
# Parent  802c1f9ec15638aaa4f1475fcbfa805d43cd6410
adapted to new PureThy.add_defs;

diff -r 802c1f9ec156 -r cf554f1c65be TFL/tfl.sml
--- a/TFL/tfl.sml	Wed Apr 29 11:33:06 1998 +0200
+++ b/TFL/tfl.sml	Wed Apr 29 11:33:27 1998 +0200
@@ -339,7 +339,7 @@
 	 Sign.infer_types (sign_of thy) (K None) (K None) [] false
 	       ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], 
 		propT)
-  in  PureThy.add_store_defs_i [(def_name, def_term)] thy  end
+  in  PureThy.add_defs_i [Attribute.none (def_name, def_term)] thy  end
 end;
 
 
@@ -459,8 +459,9 @@
      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 = PureThy.add_store_defs_i [(Name ^ "_def", subst_free[(R1,R')] proto_def)]
-	                     thy
+     val theory =
+       thy
+       |> PureThy.add_defs_i [Attribute.none (Name ^ "_def", subst_free[(R1,R')] proto_def)];
      val def = freezeT((get_axiom theory (Name ^ "_def")) RS meta_eq_to_obj_eq)
      val fconst = #lhs(S.dest_eq(concl def)) 
      val tych = Thry.typecheck theory