--- a/src/ZF/Datatype.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/Datatype.ML Fri Jul 15 13:34:31 1994 +0200
@@ -17,6 +17,7 @@
structure Inductive = Inductive_Fun
(val thy = con_thy;
+ val thy_name = thy_name;
val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs);
val sintrs = sintrs;
val monos = monos;
@@ -38,6 +39,7 @@
structure CoInductive = CoInductive_Fun
(val thy = con_thy;
+ val thy_name = thy_name;
val rec_doms = (map #1 rec_specs) ~~ (map #2 rec_specs);
val sintrs = sintrs;
val monos = monos;
--- a/src/ZF/Fin.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/Fin.ML Fri Jul 15 13:34:31 1994 +0200
@@ -17,6 +17,7 @@
structure Fin = Inductive_Fun
(val thy = Arith.thy |> add_consts [("Fin", "i=>i", NoSyn)]
+ val thy_name = "Fin"
val rec_doms = [("Fin","Pow(A)")]
val sintrs = ["0 : Fin(A)",
"[| a: A; b: Fin(A) |] ==> cons(a,b) : Fin(A)"]
@@ -25,8 +26,6 @@
val type_intrs = [empty_subsetI, cons_subsetI, PowI]
val type_elims = [make_elim PowD]);
-store_theory "Fin" Fin.thy;
-
val [Fin_0I, Fin_consI] = Fin.intrs;
--- a/src/ZF/List.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/List.ML Fri Jul 15 13:34:31 1994 +0200
@@ -8,6 +8,7 @@
structure List = Datatype_Fun
(val thy = Univ.thy
+ val thy_name = "List"
val rec_specs = [("list", "univ(A)",
[(["Nil"], "i", NoSyn),
(["Cons"], "[i,i]=>i", NoSyn)])]
@@ -18,8 +19,6 @@
val type_intrs = datatype_intrs
val type_elims = datatype_elims);
-store_theory "List" List.thy;
-
val [NilI, ConsI] = List.intrs;
(*An elimination rule, for type-checking*)
--- a/src/ZF/constructor.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/constructor.ML Fri Jul 15 13:34:31 1994 +0200
@@ -22,6 +22,7 @@
signature CONSTRUCTOR =
sig
val thy : theory (*parent theory*)
+ val thy_name : string (*name of generated theory*)
val rec_specs : (string * string * (string list * string * mixfix)list) list
(*recursion ops, types, domains, constructors*)
val rec_styp : string (*common type of all recursion ops*)
--- a/src/ZF/ex/Acc.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/Acc.ML Fri Jul 15 13:34:31 1994 +0200
@@ -11,6 +11,7 @@
structure Acc = Inductive_Fun
(val thy = WF.thy |> add_consts [("acc","i=>i",NoSyn)]
+ val thy_name = "Acc"
val rec_doms = [("acc", "field(r)")]
val sintrs = ["[| r-``{a}: Pow(acc(r)); a: field(r) |] ==> a: acc(r)"]
val monos = [Pow_mono]
--- a/src/ZF/ex/BT.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/BT.ML Fri Jul 15 13:34:31 1994 +0200
@@ -8,6 +8,7 @@
structure BT = Datatype_Fun
(val thy = Univ.thy;
+ val thy_name = "BT";
val rec_specs =
[("bt", "univ(A)",
[(["Lf"],"i",NoSyn),
--- a/src/ZF/ex/Bin.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/Bin.ML Fri Jul 15 13:34:31 1994 +0200
@@ -9,6 +9,7 @@
(*Example of a datatype with an infix constructor*)
structure Bin = Datatype_Fun
(val thy = Univ.thy;
+ val thy_name = "Bin";
val rec_specs =
[("bin", "univ(0)",
[(["Plus", "Minus"], "i", NoSyn),
--- a/src/ZF/ex/CoUnit.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/CoUnit.ML Fri Jul 15 13:34:31 1994 +0200
@@ -14,6 +14,7 @@
*)
structure CoUnit = CoDatatype_Fun
(val thy = QUniv.thy;
+ val thy_name = "CoUnit";
val rec_specs =
[("counit", "quniv(0)",
[(["Con"], "i=>i", NoSyn)])];
@@ -50,6 +51,7 @@
structure CoUnit2 = CoDatatype_Fun
(val thy = QUniv.thy;
+ val thy_name = "CoUnit2";
val rec_specs =
[("counit2", "quniv(0)",
[(["Con2"], "[i,i]=>i", NoSyn)])];
--- a/src/ZF/ex/Comb.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/Comb.ML Fri Jul 15 13:34:31 1994 +0200
@@ -14,6 +14,7 @@
(*Example of a datatype with mixfix syntax for some constructors*)
structure Comb = Datatype_Fun
(val thy = Univ.thy;
+ val thy_name = "Comb";
val rec_specs =
[("comb", "univ(0)",
[(["K","S"], "i", NoSyn),
--- a/src/ZF/ex/Contract0.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/Contract0.ML Fri Jul 15 13:34:31 1994 +0200
@@ -10,6 +10,7 @@
structure Contract = Inductive_Fun
(val thy = Contract0.thy;
+ val thy_name = "Contract";
val rec_doms = [("contract","comb*comb")];
val sintrs =
["[| p:comb; q:comb |] ==> K#p#q -1-> p",
--- a/src/ZF/ex/Data.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/Data.ML Fri Jul 15 13:34:31 1994 +0200
@@ -9,6 +9,7 @@
structure Data = Datatype_Fun
(val thy = Univ.thy
+ val thy_name = "Data"
val rec_specs = [("data", "univ(A Un B)",
[(["Con0"], "i",NoSyn),
(["Con1"], "i=>i",NoSyn),
--- a/src/ZF/ex/Enum.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/Enum.ML Fri Jul 15 13:34:31 1994 +0200
@@ -17,6 +17,7 @@
structure Enum = Datatype_Fun
(val thy = Univ.thy;
+ val thy_name = "Enum";
val rec_specs =
[("enum", "univ(0)",
[(consts, "i", NoSyn)])];
--- a/src/ZF/ex/LList.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/LList.ML Fri Jul 15 13:34:31 1994 +0200
@@ -8,6 +8,7 @@
structure LList = CoDatatype_Fun
(val thy = QUniv.thy
+ val thy_name = "LList"
val rec_specs = [("llist", "quniv(A)",
[(["LNil"], "i",NoSyn),
(["LCons"], "[i,i]=>i",NoSyn)])]
--- a/src/ZF/ex/LList_Eq.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/LList_Eq.ML Fri Jul 15 13:34:31 1994 +0200
@@ -12,6 +12,7 @@
structure LList_Eq = CoInductive_Fun
(val thy = LList.thy |> add_consts [("lleq","i=>i",NoSyn)]
+ val thy_name = "LList_Eq"
val rec_doms = [("lleq", "llist(A) * llist(A)")]
val sintrs =
["<LNil, LNil> : lleq(A)",
--- a/src/ZF/ex/ListN.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/ListN.ML Fri Jul 15 13:34:31 1994 +0200
@@ -11,6 +11,7 @@
structure ListN = Inductive_Fun
(val thy = ListFn.thy |> add_consts [("listn","i=>i",NoSyn)]
+ val thy_name = "ListN"
val rec_doms = [("listn", "nat*list(A)")]
val sintrs =
["<0,Nil> : listn(A)",
--- a/src/ZF/ex/ParContract.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/ParContract.ML Fri Jul 15 13:34:31 1994 +0200
@@ -11,6 +11,7 @@
structure ParContract = Inductive_Fun
(val thy = Contract.thy;
+ val thy_name = "ParContract";
val rec_doms = [("parcontract","comb*comb")];
val sintrs =
["[| p:comb |] ==> p =1=> p",
--- a/src/ZF/ex/Primrec0.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/Primrec0.ML Fri Jul 15 13:34:31 1994 +0200
@@ -65,6 +65,7 @@
structure Primrec = Inductive_Fun
(val thy = Primrec0.thy
+ val thy_name = "Primrec"
val rec_doms = [("primrec", "list(nat)->nat")]
val sintrs =
["SC : primrec",
--- a/src/ZF/ex/Prop.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/Prop.ML Fri Jul 15 13:34:31 1994 +0200
@@ -10,6 +10,7 @@
(*Example of a datatype with mixfix syntax for some constructors*)
structure Prop = Datatype_Fun
(val thy = Univ.thy;
+ val thy_name = "Prop";
val rec_specs =
[("prop", "univ(0)",
[(["Fls"], "i",NoSyn),
--- a/src/ZF/ex/PropLog.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/PropLog.ML Fri Jul 15 13:34:31 1994 +0200
@@ -78,6 +78,7 @@
structure PropThms = Inductive_Fun
(val thy = PropLog.thy;
+ val thy_name = "PropThms";
val rec_doms = [("thms","prop")];
val sintrs =
["[| p:H; p:prop |] ==> H |- p",
--- a/src/ZF/ex/Rmap.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/Rmap.ML Fri Jul 15 13:34:31 1994 +0200
@@ -8,6 +8,7 @@
structure Rmap = Inductive_Fun
(val thy = List.thy |> add_consts [("rmap","i=>i",NoSyn)];
+ val thy_name = "Rmap";
val rec_doms = [("rmap", "list(domain(r))*list(range(r))")];
val sintrs =
["<Nil,Nil> : rmap(r)",
--- a/src/ZF/ex/TF.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/TF.ML Fri Jul 15 13:34:31 1994 +0200
@@ -8,6 +8,7 @@
structure TF = Datatype_Fun
(val thy = Univ.thy
+ val thy_name = "TF"
val rec_specs = [("tree", "univ(A)",
[(["Tcons"], "[i,i]=>i",NoSyn)]),
("forest", "univ(A)",
--- a/src/ZF/ex/Term.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/ex/Term.ML Fri Jul 15 13:34:31 1994 +0200
@@ -9,6 +9,7 @@
structure Term = Datatype_Fun
(val thy = List.thy;
+ val thy_name = "Term";
val rec_specs =
[("term", "univ(A)",
[(["Apply"], "[i,i]=>i", NoSyn)])];
--- a/src/ZF/intr_elim.ML Fri Jul 15 13:30:42 1994 +0200
+++ b/src/ZF/intr_elim.ML Fri Jul 15 13:34:31 1994 +0200
@@ -65,6 +65,7 @@
signature INDUCTIVE = (** Description of a (co)inductive defn **)
sig
val thy : theory (*parent theory*)
+ val thy_name : string (*name of generated theory*)
val rec_doms : (string*string) list (*recursion ops and their domains*)
val sintrs : string list (*desired introduction rules*)
val monos : thm list (*monotonicity of each M operator*)
@@ -76,6 +77,7 @@
signature INTR_ELIM =
sig
val thy : theory (*new theory*)
+ val thy_name : string (*name of generated theory*)
val defs : thm list (*definitions made in thy*)
val bnd_mono : thm (*monotonicity for the lfp definition*)
val unfold : thm (*fixed-point equation*)
@@ -210,7 +212,7 @@
val thy =
Ind.thy
|> add_axioms_i axpairs
- |> add_thyname (big_rec_name ^ "_Inductive");
+ |> add_thyname thy_name;
val defs = map (get_axiom thy o #1) axpairs;