src/HOLCF/domain/theorems.ML
changeset 4861 7ed04b370b71
parent 4755 843b5f159c7e
child 5291 5706f0ef1d43
     1.1 --- a/src/HOLCF/domain/theorems.ML	Wed Apr 29 11:35:24 1998 +0200
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Wed Apr 29 11:36:08 1998 +0200
     1.3 @@ -323,7 +323,7 @@
     1.4                          (filter (fn (_,args)=>exists is_nonlazy_rec args) cons);
     1.5  val copy_rews = copy_strict::copy_apps @ copy_stricts;
     1.6  in thy |> Theory.add_path (Sign.base_name dname)
     1.7 -       |> PureThy.store_thmss [
     1.8 +       |> (PureThy.add_tthmss o map Attribute.no_attrss) [
     1.9  		("iso_rews" , iso_rews  ),
    1.10  		("exhaust"  , [exhaust] ),
    1.11  		("casedist" , [casedist]),
    1.12 @@ -336,7 +336,7 @@
    1.13  		("inverts" , inverts ),
    1.14  		("injects" , injects ),
    1.15  		("copy_rews", copy_rews)]
    1.16 -       |> Theory.add_path ".."
    1.17 +       |> Theory.parent_path
    1.18  end; (* let *)
    1.19  
    1.20  fun comp_theorems (comp_dnam, eqs: eq list) thy =
    1.21 @@ -598,14 +598,14 @@
    1.22  
    1.23  
    1.24  in thy |> Theory.add_path comp_dnam
    1.25 -       |> PureThy.store_thmss [
    1.26 +       |> (PureThy.add_tthmss o map Attribute.no_attrss) [
    1.27  		("take_rews"  , take_rews  ),
    1.28  		("take_lemmas", take_lemmas),
    1.29  		("finites"    , finites    ),
    1.30  		("finite_ind", [finite_ind]),
    1.31  		("ind"       , [ind       ]),
    1.32  		("coind"     , [coind     ])]
    1.33 -       |> Theory.add_path ".."
    1.34 +       |> Theory.parent_path
    1.35  end; (* let *)
    1.36  end; (* local *)
    1.37  end; (* struct *)