src/ZF/constructor.ML
changeset 477 53fc8ad84b33
parent 466 08d1cce222e1
child 516 1957113f0d7d
--- 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*)