--- a/src/HOLCF/domain/theorems.ML Wed Apr 29 11:35:24 1998 +0200
+++ b/src/HOLCF/domain/theorems.ML Wed Apr 29 11:36:08 1998 +0200
@@ -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.store_thmss [
+ |> (PureThy.add_tthmss o map Attribute.no_attrss) [
("iso_rews" , iso_rews ),
("exhaust" , [exhaust] ),
("casedist" , [casedist]),
@@ -336,7 +336,7 @@
("inverts" , inverts ),
("injects" , injects ),
("copy_rews", copy_rews)]
- |> Theory.add_path ".."
+ |> Theory.parent_path
end; (* let *)
fun comp_theorems (comp_dnam, eqs: eq list) thy =
@@ -598,14 +598,14 @@
in thy |> Theory.add_path comp_dnam
- |> PureThy.store_thmss [
+ |> (PureThy.add_tthmss o map Attribute.no_attrss) [
("take_rews" , take_rews ),
("take_lemmas", take_lemmas),
("finites" , finites ),
("finite_ind", [finite_ind]),
("ind" , [ind ]),
("coind" , [coind ])]
- |> Theory.add_path ".."
+ |> Theory.parent_path
end; (* let *)
end; (* local *)
end; (* struct *)