src/ZF/ex/CoUnit.ML

   definition is trivial!  The same thing occurs with Aczel's Special Final
   Coalgebra Theorem
 *)
 structure CoUnit = CoDatatype_Fun
  (val thy = QUniv.thy;
+  val thy_name = "CoUnit";
   val rec_specs = 
       [("counit", "quniv(0)",
 	  [(["Con"],	"i=>i", NoSyn)])];
   val rec_styp = "i";
   val sintrs = ["x: counit ==> Con(x) : counit"];

   The resulting set is a singleton.
 *)
 
 structure CoUnit2 = CoDatatype_Fun
  (val thy = QUniv.thy;
+  val thy_name = "CoUnit2";
   val rec_specs = 
       [("counit2", "quniv(0)",
 	  [(["Con2"],	"[i,i]=>i", NoSyn)])];
   val rec_styp = "i";
   val sintrs = ["[| x: counit2;  y: counit2 |] ==> Con2(x,y) : counit2"];