# HG changeset patch
# User paulson
# Date 906725187 -7200
# Node ID 0067dd151d7a9defc67bc37a8a71f4411da7ccc7
# Parent  99c6ef61288fe14ca8104583634152627a9eb7c4
added Int to BasisLibrary

diff -r 99c6ef61288f -r 0067dd151d7a src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Fri Sep 25 14:06:00 1998 +0200
+++ b/src/Pure/ROOT.ML	Fri Sep 25 14:06:27 1998 +0200
@@ -60,11 +60,12 @@
 (*if true then some packages won't be too serious about actually proving things*)
 val quick_and_dirty = ref false;
 
-(*several object-logics declare theories named List or Option, hiding
-  the eponymous basis library structures*)
+(*several object-logics declare theories that hide basis library structures*)
 structure BasisLibrary =
 struct
-  structure List = List and Option = Option;
+  structure List   = List 
+  and       Option = Option
+  and       Int    = Int;
 end;
 
 open Use;