# HG changeset patch
# User wenzelm
# Date 875722421 -7200
# Node ID 67f4ac7591003c8b21b8064f0526b502b7504460
# Parent  e2bb53d8dd2642b08a61611ced0e2112608b9e49
fully qualified names: Theory.add_XXX;

diff -r e2bb53d8dd26 -r 67f4ac759100 TFL/tfl.sml
--- a/TFL/tfl.sml	Wed Oct 01 17:43:42 1997 +0200
+++ b/TFL/tfl.sml	Wed Oct 01 18:13:41 1997 +0200
@@ -338,7 +338,7 @@
 	 Sign.infer_types (sign_of thy) (K None) (K None) [] false
 	       ([Const("==",dummyT) $ Const(Name,Ty) $ wfrec_R_M], 
 		propT)
-  in  add_defs_i [(def_name, def_term)] thy  end
+  in  Theory.add_defs_i [(def_name, def_term)] thy  end
 end;
 
 
@@ -458,7 +458,7 @@
      val full_rqt = WFR::TCs
      val R' = S.mk_select{Bvar=R1, Body=S.list_mk_conj full_rqt}
      val R'abs = S.rand R'
-     val theory = add_defs_i [(Name ^ "_def", subst_free[(R1,R')] proto_def)]
+     val theory = Theory.add_defs_i [(Name ^ "_def", subst_free[(R1,R')] proto_def)]
 	                     thy
      val def = freezeT((get_axiom theory (Name ^ "_def")) RS meta_eq_to_obj_eq)
      val fconst = #lhs(S.dest_eq(concl def)) 
diff -r e2bb53d8dd26 -r 67f4ac759100 src/HOL/Inductive.ML
--- a/src/HOL/Inductive.ML	Wed Oct 01 17:43:42 1997 +0200
+++ b/src/HOL/Inductive.ML	Wed Oct 01 18:13:41 1997 +0200
@@ -75,7 +75,7 @@
     val rec_tms = map (readtm sign termTVar) srec_tms
     and intr_tms = map (readtm sign propT) sintrs;
     val thy = thy |> Ind.add_fp_def_i(rec_tms, intr_tms) 
-                  |> add_thyname thy_name);
+                  |> Theory.add_name thy_name);
 
 
 
diff -r e2bb53d8dd26 -r 67f4ac759100 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Wed Oct 01 17:43:42 1997 +0200
+++ b/src/HOL/NatDef.ML	Wed Oct 01 18:13:41 1997 +0200
@@ -724,6 +724,5 @@
 (* add function nat_add_primrec *) 
 val (_, nat_add_primrec, _) = Datatype.add_datatype
 ([], "nat", [("0", [], Mixfix ("0", [], max_pri)), ("Suc", [dtTyp ([],
-"nat")], NoSyn)]) (add_thyname "Arith" HOL.thy);
-(* pretend Arith is part of the basic theory to fool package *)
-
+"nat")], NoSyn)]) (Theory.add_name "Arith" HOL.thy);
+(*pretend Arith is part of the basic theory to fool package*)
diff -r e2bb53d8dd26 -r 67f4ac759100 src/HOL/add_ind_def.ML
--- a/src/HOL/add_ind_def.ML	Wed Oct 01 17:43:42 1997 +0200
+++ b/src/HOL/add_ind_def.ML	Wed Oct 01 18:13:41 1997 +0200
@@ -157,7 +157,7 @@
              | x::_ => error ("Illegal occurrence of recursion op: " ^ x ^
                                "\n\t*Consider adding type constraints*"))
 
-  in  thy |> add_defs_i axpairs  end
+  in  thy |> Theory.add_defs_i axpairs  end
 
 
 (****************************************************************OMITTED
@@ -240,10 +240,6 @@
 *   val axpairs =
         big_case_def :: flat (ListPair.map mk_con_defs ((1 upto npart), con_ty_lists))
 
-*   in  thy |> add_consts_i const_decs |> add_defs_i axpairs  end;
+*   in  thy |> Theory.add_consts_i const_decs |> Theory.add_defs_i axpairs  end;
 ****************************************************************)
 end;
-
-
-
-
diff -r e2bb53d8dd26 -r 67f4ac759100 src/HOL/datatype.ML
--- a/src/HOL/datatype.ML	Wed Oct 01 17:43:42 1997 +0200
+++ b/src/HOL/datatype.ML	Wed Oct 01 18:13:41 1997 +0200
@@ -504,14 +504,14 @@
           val defpairT as (_, _ $ Const(_,T) $ _ ) = inferT_axm sg defpair;
           val varT = Type.varifyT T;
           val ftyp = the (Sign.const_type sg fname);
-        in add_defs_i [defpairT] thy end;
+        in Theory.add_defs_i [defpairT] thy end;
 
     in
-      (thy |> add_types types
-           |> add_arities arities
-           |> add_consts consts
-           |> add_trrules xrules
-           |> add_axioms rules, add_primrec, size_eqns)
+      (thy |> Theory.add_types types
+           |> Theory.add_arities arities
+           |> Theory.add_consts consts
+           |> Theory.add_trrules xrules
+           |> Theory.add_axioms rules, add_primrec, size_eqns)
     end
 
 (*Warn if the (induction) variable occurs Free among the premises, which
diff -r e2bb53d8dd26 -r 67f4ac759100 src/HOL/typedef.ML
--- a/src/HOL/typedef.ML	Wed Oct 01 17:43:42 1997 +0200
+++ b/src/HOL/typedef.ML	Wed Oct 01 18:13:41 1997 +0200
@@ -107,17 +107,17 @@
     prove_nonempty cset (map (get_axiom thy) axms @ thms) usr_tac;
 
     thy
-    |> add_types [(t, tlen, mx)]
-    |> add_arities
+    |> Theory.add_types [(t, tlen, mx)]
+    |> Theory.add_arities
      [(tname, replicate tlen logicS, logicS),
       (tname, replicate tlen termS, termS)]
-    |> add_consts_i
+    |> Theory.add_consts_i
      [(name, setT, NoSyn),
       (Rep_name, newT --> oldT, NoSyn),
       (Abs_name, oldT --> newT, NoSyn)]
-    |> add_defs_i
+    |> Theory.add_defs_i
      [(name ^ "_def", mk_equals (setC, set))]
-    |> add_axioms_i
+    |> Theory.add_axioms_i
      [(Rep_name, rep_type),
       (Rep_name ^ "_inverse", rep_type_inv),
       (Abs_name ^ "_inverse", abs_type_inv)]
diff -r e2bb53d8dd26 -r 67f4ac759100 src/LCF/ex/ex.ML
--- a/src/LCF/ex/ex.ML	Wed Oct 01 17:43:42 1997 +0200
+++ b/src/LCF/ex/ex.ML	Wed Oct 01 18:13:41 1997 +0200
@@ -11,16 +11,16 @@
 
 val ex_thy =
   thy
-  |> add_consts
+  |> Theory.add_consts
    [("P", "'a => tr", NoSyn),
     ("G", "'a => 'a", NoSyn),
     ("H", "'a => 'a", NoSyn),
     ("K", "('a => 'a) => ('a => 'a)", NoSyn)]
-  |> add_axioms
+  |> Theory.add_axioms
    [("P_strict", "P(UU) = UU"),
     ("K", "K = (%h x. P(x) => x | h(h(G(x))))"),
     ("H", "H = FIX(K)")]
-  |> add_thyname "Ex 10.4";
+  |> Theory.add_name "Ex 10.4";
 
 val ax = get_axiom ex_thy;
 
@@ -55,17 +55,17 @@
 
 val ex_thy =
   thy
-  |> add_consts
+  |> Theory.add_consts
    [("P", "'a => tr", NoSyn),
     ("F", "'a => 'a", NoSyn),
     ("G", "'a => 'a", NoSyn),
     ("H", "'a => 'b => 'b", NoSyn),
     ("K", "('a => 'b => 'b) => ('a => 'b => 'b)", NoSyn)]
-  |> add_axioms
+  |> Theory.add_axioms
    [("F_strict", "F(UU) = UU"),
     ("K", "K = (%h x y. P(x) => y | F(h(G(x),y)))"),
     ("H", "H = FIX(K)")]
-  |> add_thyname "Ex 3.8";
+  |> Theory.add_name "Ex 3.8";
 
 val ax = get_axiom ex_thy;
 
@@ -87,13 +87,13 @@
 
 val ex_thy =
   thy
-  |> add_consts
+  |> Theory.add_consts
    [("s", "'a => 'a", NoSyn),
     ("p", "'a => 'a => 'a", NoSyn)]
-  |> add_axioms
+  |> Theory.add_axioms
    [("p_strict", "p(UU) = UU"),
     ("p_s", "p(s(x),y) = s(p(x,y))")]
-  |> add_thyname "fix ex";
+  |> Theory.add_name "fix ex";
 
 val ax = get_axiom ex_thy;
 
diff -r e2bb53d8dd26 -r 67f4ac759100 src/ZF/add_ind_def.ML
--- a/src/ZF/add_ind_def.ML	Wed Oct 01 17:43:42 1997 +0200
+++ b/src/ZF/add_ind_def.ML	Wed Oct 01 18:13:41 1997 +0200
@@ -162,7 +162,7 @@
 
     val dummy = seq (writeln o Sign.string_of_term sign o #2) axpairs
   
-  in  thy |> add_defs_i axpairs  end
+  in  thy |> Theory.add_defs_i axpairs  end
 
 
 (*Expects the recursive sets to have been defined already.
@@ -250,5 +250,5 @@
         big_case_def :: flat (ListPair.map mk_con_defs
 			      (1 upto npart, con_ty_lists))
 
-    in  thy |> add_consts_i const_decs |> add_defs_i axpairs  end;
+    in  thy |> Theory.add_consts_i const_decs |> Theory.add_defs_i axpairs  end;
 end;