src/Pure/ROOT.ML
changeset 5607 5db9e2343ade
parent 5568 0067dd151d7a
child 5684 9a3acc4c7c2e
     1.1 --- a/src/Pure/ROOT.ML	Fri Oct 02 10:43:08 1998 +0200
     1.2 +++ b/src/Pure/ROOT.ML	Fri Oct 02 10:44:20 1998 +0200
     1.3 @@ -65,7 +65,9 @@
     1.4  struct
     1.5    structure List   = List 
     1.6    and       Option = Option
     1.7 -  and       Int    = Int;
     1.8 +  and       Bool   = Bool
     1.9 +  and       Int    = Int
    1.10 +  and       Real   = Real;
    1.11  end;
    1.12  
    1.13  open Use;