--- a/TFL/tfl.sml Tue Jan 12 13:40:08 1999 +0100
+++ b/TFL/tfl.sml Tue Jan 12 13:54:51 1999 +0100
@@ -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_defs_i [Attribute.none (def_name, def_term)] thy end
+ in PureThy.add_defs_i [Thm.no_attributes (def_name, def_term)] thy end
end;
@@ -461,7 +461,7 @@
val R'abs = S.rand R'
val theory =
thy
- |> PureThy.add_defs_i [Attribute.none (Name ^ "_def", subst_free[(R1,R')] proto_def)];
+ |> PureThy.add_defs_i [Thm.no_attributes (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