src/HOLCF/domain/theorems.ML

                          in map (case_UU_tac rews 1) (nonlazy args) @ [
                              asm_simp_tac (HOLCF_ss addsimps rews) 1] end))
                         (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]),
 		("when_rews", when_rews ),
 		("con_rews", con_rews),

 		("dis_rews", dis_rews),
 		("dist_les", dist_les),
 		("dist_eqs", dist_eqs),
 		("inverts" , inverts ),
 		("injects" , injects ),
-		("copy_rews", copy_rews)]
+		("copy_rews", copy_rews)])))
        |> Theory.parent_path
 end; (* let *)
 
 fun comp_theorems (comp_dnam, eqs: eq list) thy =
 let

                                 take_lemmas));
 end; (* local *)
 
 
 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 *)
 end; (* struct *)