--- a/src/HOLCF/domain/theorems.ML Tue Jan 12 13:40:08 1999 +0100
+++ b/src/HOLCF/domain/theorems.ML Tue Jan 12 13:54:51 1999 +0100
@@ -323,7 +323,7 @@
(filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
val copy_rews = copy_strict::copy_apps @ copy_stricts;
in thy |> Theory.add_path (Sign.base_name dname)
- |> (PureThy.add_tthmss o map Attribute.no_attrss) [
+ |> (PureThy.add_thmss o map Thm.no_attributes) [
("iso_rews" , iso_rews ),
("exhaust" , [exhaust] ),
("casedist" , [casedist]),
@@ -598,7 +598,7 @@
in thy |> Theory.add_path comp_dnam
- |> (PureThy.add_tthmss o map Attribute.no_attrss) [
+ |> (PureThy.add_thmss o map Thm.no_attributes) [
("take_rews" , take_rews ),
("take_lemmas", take_lemmas),
("finites" , finites ),