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))