--- 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))
--- 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);
--- 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*)
--- 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;
-
-
-
-
--- 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
--- 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)]
--- 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;
--- 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;