src/ZF/Datatype.ML
changeset 477 53fc8ad84b33
parent 120 09287f26bfb8
child 516 1957113f0d7d
--- 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;