# HG changeset patch
# User wenzelm
# Date 875825640 -7200
# Node ID ede66fb9988049c6932ffe7183b76f9bc16c40d5
# Parent  294b5905f4ebff3a2ff577f4c77f7f4181a93eef
fully qualified names: Theory.add_XXX;

diff -r 294b5905f4eb -r ede66fb99880 src/Cube/Cube.ML
--- a/src/Cube/Cube.ML	Wed Oct 01 18:19:44 1997 +0200
+++ b/src/Cube/Cube.ML	Thu Oct 02 22:54:00 1997 +0200
@@ -12,11 +12,11 @@
 
 val L2_thy =
   Cube.thy
-  |> add_axioms
+  |> Theory.add_axioms
    [("pi_bs",  "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"),
     ("lam_bs", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \
      \  ==> Abs(A,f) : Prod(A,B)")]
-  |> add_thyname "L2";
+  |> Theory.add_name "L2";
 
 val lam_bs = get_axiom L2_thy "lam_bs";
 val pi_bs = get_axiom L2_thy "pi_bs";
@@ -25,11 +25,11 @@
 
 val Lomega_thy =
   Cube.thy
-  |> add_axioms
+  |> Theory.add_axioms
    [("pi_bb",  "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
     ("lam_bb", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
      \  ==> Abs(A,f) : Prod(A,B)")]
-  |> add_thyname "Lomega";
+  |> Theory.add_name "Lomega";
 
 val lam_bb = get_axiom Lomega_thy "lam_bb";
 val pi_bb = get_axiom Lomega_thy "pi_bb";
@@ -40,11 +40,11 @@
 
 val LP_thy =
   Cube.thy
-  |> add_axioms
+  |> Theory.add_axioms
    [("pi_sb",  "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
     ("lam_sb", "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
      \  ==> Abs(A,f) : Prod(A,B)")]
-  |> add_thyname "LP";
+  |> Theory.add_name "LP";
 
 val lam_sb = get_axiom LP_thy "lam_sb";
 val pi_sb = get_axiom LP_thy "pi_sb";
diff -r 294b5905f4eb -r ede66fb99880 src/HOLCF/ax_ops/thy_axioms.ML
--- a/src/HOLCF/ax_ops/thy_axioms.ML	Wed Oct 01 18:19:44 1997 +0200
+++ b/src/HOLCF/ax_ops/thy_axioms.ML	Thu Oct 02 22:54:00 1997 +0200
@@ -148,7 +148,7 @@
   let val {sign, ...} = rep_theory theory;
       val constraints = get_constraints_of_str sign (defvarlist@varlist)
   in
-    add_axioms_i (map (apsnd 
+    Theory.add_axioms_i (map (apsnd 
      (check_and_extend sign (map fst defvarlist) (map fst varlist)) o
                (read_ext_axm sign constraints)) axioms) theory
   end 
@@ -157,7 +157,7 @@
   let val {sign, ...} = rep_theory theory;
       val constraints = get_constraints_of_typ sign (defvarlist@varlist)
   in
-    add_axioms_i (map (apsnd (check_and_extend sign 
+    Theory.add_axioms_i (map (apsnd (check_and_extend sign 
                                (map fst defvarlist) (map fst varlist)) o
                    (read_ext_axm_terms sign constraints)) axiom_terms) theory
   end
diff -r 294b5905f4eb -r ede66fb99880 src/HOLCF/ax_ops/thy_ops.ML
--- a/src/HOLCF/ax_ops/thy_ops.ML	Wed Oct 01 18:19:44 1997 +0200
+++ b/src/HOLCF/ax_ops/thy_ops.ML	Thu Oct 02 22:54:00 1997 +0200
@@ -342,8 +342,8 @@
       val s_axms = (if strict then strictness_axms curried decls else []);
       val t_axms = (if total  then totality_axms   curried decls else []);
   in 
-  add_trrules_i xrules (add_axioms_i (s_axms @ t_axms) 
-                     (add_syntax_i syndecls (add_consts_i oldstyledecls thy)))
+  Theory.add_trrules_i xrules (Theory.add_axioms_i (s_axms @ t_axms) 
+                     (Theory.add_syntax_i syndecls (Theory.add_consts_i oldstyledecls thy)))
   end;
 
 fun add_ops_i {curried,strict,total} decls thy =
@@ -354,8 +354,8 @@
       val s_axms = (if strict then strictness_axms curried decls else []);
       val t_axms = (if total  then totality_axms   curried decls else []);
   in 
-  add_trrules_i xrules (add_axioms_i (s_axms @ t_axms) 
-                     (add_syntax_i syndecls (add_consts_i oldstyledecls thy)))
+  Theory.add_trrules_i xrules (Theory.add_axioms_i (s_axms @ t_axms) 
+                     (Theory.add_syntax_i syndecls (Theory.add_consts_i oldstyledecls thy)))
   end;
 
 
diff -r 294b5905f4eb -r ede66fb99880 src/HOLCF/domain/axioms.ML
--- a/src/HOLCF/domain/axioms.ML	Wed Oct 01 18:19:44 1997 +0200
+++ b/src/HOLCF/domain/axioms.ML	Thu Oct 02 22:54:00 1997 +0200
@@ -123,7 +123,7 @@
     in foldr' mk_conj (mapn one_comp 0 eqs)end ));
   val thy_axs = flat (mapn (calc_axioms comp_dname eqs) 0 eqs) @
 		(if length eqs>1 then [ax_copy_def] else []) @ [ax_bisim_def];
-in thy' |> add_axioms_i (infer_types thy' thy_axs) end;
+in thy' |> Theory.add_axioms_i (infer_types thy' thy_axs) end;
 
 
 fun add_induct ((tname,finite),(typs,cnstrs)) thy' = let
@@ -143,7 +143,7 @@
   val concl = mk_trp(foldr' mk_conj (map one_conc typs));
   val induct = (tname^"_induct",lift_adm(lift_pred_UU(
 			foldr (op ===>) (map one_cnstr cnstrs,concl))));
-in thy' |> add_axioms_i (infer_types thy' [induct]) end;
+in thy' |> Theory.add_axioms_i (infer_types thy' [induct]) end;
 
 end; (* local *)
 end; (* struct *)
diff -r 294b5905f4eb -r ede66fb99880 src/HOLCF/domain/syntax.ML
--- a/src/HOLCF/domain/syntax.ML	Wed Oct 01 18:19:44 1997 +0200
+++ b/src/HOLCF/domain/syntax.ML	Thu Oct 02 22:54:00 1997 +0200
@@ -115,11 +115,11 @@
   val const_bisim  = (comp_dname^"_bisim" ,relprod --> HOLogic.boolT, NoSyn');
   val ctt           = map (calc_syntax funprod) eqs';
   val add_cur_ops_i = ThyOps.add_ops_i {curried=true, strict=false, total=false};
-in thy'' |> add_types      thy_types
-	 |> add_arities    thy_arities
+in thy'' |> Theory.add_types      thy_types
+	 |> Theory.add_arities    thy_arities
 	 |> add_cur_ops_i (flat(map fst ctt))
 	 |> add_cur_ops_i ((if length eqs'>1 then [const_copy] else[])@[const_bisim])
-	 |> add_trrules_i (flat(map snd ctt))
+	 |> Theory.add_trrules_i (flat(map snd ctt))
 end; (* let *)
 
 end; (* local *)