# HG changeset patch
# User wenzelm
# Date 893842613 -7200
# Node ID 613ce4cc303fa5284cf82845a468c091b341d063
# Parent  7ed04b370b71dcfe2bae0558c5fcb869304fdb2d
adapted to new PureThy.add_axioms_i;
Theory.parent_path;

diff -r 7ed04b370b71 -r 613ce4cc303f src/HOLCF/domain/axioms.ML
--- a/src/HOLCF/domain/axioms.ML	Wed Apr 29 11:36:08 1998 +0200
+++ b/src/HOLCF/domain/axioms.ML	Wed Apr 29 11:36:53 1998 +0200
@@ -86,6 +86,7 @@
     [take_def, finite_def])
 end; (* let *)
 
+val add_axioms_i = PureThy.add_axioms_i o map Attribute.none;
 
 in (* local *)
 
@@ -126,14 +127,14 @@
     in foldr' mk_conj (mapn one_comp 0 eqs)end ));
   fun add_one (thy,(dnam,axs,dfs)) = thy 
 	|> Theory.add_path dnam
-	|> PureThy.add_store_axioms_i (infer_types thy' dfs)(*add_store_defs_i*)
-	|> PureThy.add_store_axioms_i (infer_types thy' axs)
-	|> Theory.add_path "..";
+	|> add_axioms_i (infer_types thy' dfs)(*add_defs_i*)
+	|> add_axioms_i (infer_types thy' axs)
+	|> Theory.parent_path;
   val thy = foldl add_one (thy', mapn (calc_axioms comp_dname eqs) 0 eqs);
 in thy |> Theory.add_path comp_dnam  
-       |> PureThy.add_store_axioms_i (infer_types thy' 
+       |> add_axioms_i (infer_types thy' 
 		(bisim_def::(if length eqs>1 then [copy_def] else [])))
-       |> Theory.add_path ".."
+       |> Theory.parent_path
 end;
 
 end; (* local *)