# HG changeset patch
# User clasohm
# Date 774272071 -7200
# Node ID 53fc8ad84b3388075eeadc06493358393eb264a6
# Parent  836cad329311780a93e929d8fac80fa62d6f4073
added thy_name to Datatype_Fun's parameter

diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/Datatype.ML
--- 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;
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/Fin.ML
--- 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;
 
 
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/List.ML
--- 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*)
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/constructor.ML
--- 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*)
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/Acc.ML
--- 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]
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/BT.ML
--- 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), 
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/Bin.ML
--- 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),
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/CoUnit.ML
--- 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)])];
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/Comb.ML
--- 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),
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/Contract0.ML
--- 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",
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/Data.ML
--- 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),
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/Enum.ML
--- 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)])];
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/LList.ML
--- 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)])]
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/LList_Eq.ML
--- 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)",
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/ListN.ML
--- 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)",
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/ParContract.ML
--- 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",
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/Primrec0.ML
--- 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",
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/Prop.ML
--- 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),
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/PropLog.ML
--- 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",
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/Rmap.ML
--- 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)",
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/TF.ML
--- 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)",
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/ex/Term.ML
--- 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)])];
diff -r 836cad329311 -r 53fc8ad84b33 src/ZF/intr_elim.ML
--- 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;