--- a/src/ZF/ex/BT.thy Tue Mar 07 13:34:33 1995 +0100 +++ b/src/ZF/ex/BT.thy Tue Mar 07 13:37:48 1995 +0100 @@ -6,7 +6,7 @@ Binary trees *) -BT = Univ + +BT = Datatype + consts bt_rec :: "[i, i, [i,i,i,i,i]=>i] => i" n_nodes :: "i=>i"