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