--- a/src/HOL/ex/BT.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/ex/BT.thy Fri Jun 17 16:12:49 2005 +0200 @@ -8,7 +8,7 @@ header {* Binary trees *} -theory BT = Main: +theory BT imports Main begin datatype 'a bt = Lf