src/ZF/ex/BT.ML

 Datatype definition of binary trees
 *)
 
 structure BT = Datatype_Fun
  (val thy = Univ.thy;
+  val thy_name = "BT";
   val rec_specs = 
       [("bt", "univ(A)",
 	  [(["Lf"],"i",NoSyn), 
            (["Br"],"[i,i,i]=>i", NoSyn)])];
   val rec_styp = "i=>i";