--- a/src/HOLCF/domain/theorems.ML Mon Mar 13 13:27:44 2000 +0100
+++ b/src/HOLCF/domain/theorems.ML Mon Mar 13 13:28:31 2000 +0100
@@ -315,7 +315,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_thmss o map Thm.no_attributes) [
+ |> (#1 o (PureThy.add_thmss (map Thm.no_attributes [
("iso_rews" , iso_rews ),
("exhaust" , [exhaust] ),
("casedist" , [casedist]),
@@ -327,7 +327,7 @@
("dist_eqs", dist_eqs),
("inverts" , inverts ),
("injects" , injects ),
- ("copy_rews", copy_rews)]
+ ("copy_rews", copy_rews)])))
|> Theory.parent_path
end; (* let *)
@@ -590,13 +590,13 @@
in thy |> Theory.add_path comp_dnam
- |> (PureThy.add_thmss o map Thm.no_attributes) [
+ |> (#1 o (PureThy.add_thmss (map Thm.no_attributes [
("take_rews" , take_rews ),
("take_lemmas", take_lemmas),
("finites" , finites ),
("finite_ind", [finite_ind]),
("ind" , [ind ]),
- ("coind" , [coind ])]
+ ("coind" , [coind ])])))
|> Theory.parent_path
end; (* let *)
end; (* local *)