src/HOL/ex/BT.thy

--- a/src/HOL/ex/BT.thy	Sat Mar 04 11:42:12 2000 +0100
+++ b/src/HOL/ex/BT.thy	Sat Mar 04 11:52:42 2000 +0100
@@ -6,9 +6,10 @@
 Binary trees (based on the ZF version)
 *)
 
-BT = List +
+BT = Main +
 
-datatype 'a bt = Lf  |  Br 'a ('a bt) ('a bt)
+datatype 'a bt = Lf
+               | Br 'a ('a bt) ('a bt)
   
 consts
     n_nodes     :: 'a bt => nat