--- a/src/Pure/ROOT.ML Fri Oct 02 10:43:08 1998 +0200+++ b/src/Pure/ROOT.ML Fri Oct 02 10:44:20 1998 +0200@@ -65,7 +65,9 @@ struct structure List = List and Option = Option- and Int = Int;+ and Bool = Bool+ and Int = Int+ and Real = Real; end; open Use;