diff -r 3692eb8a6cdb -r 7ed04b370b71 src/HOLCF/domain/theorems.ML
--- 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 *)