Declares List_ as a synonym for List

--- a/src/Pure/library.ML	Thu Nov 28 12:31:33 1996 +0100
+++ b/src/Pure/library.ML	Thu Nov 28 12:36:31 1996 +0100
@@ -112,6 +112,10 @@
 fun andl [] = true
   | andl (x :: xs) = x andalso andl xs;
 
+(*Needed because several object-logics declare the theory, therefore structure,
+  List.*)
+structure List_ = List;
+
 (*exists pred [x1, ..., xn] ===> pred x1 orelse ... orelse pred xn*)
 fun exists (pred: 'a -> bool) : 'a list -> bool =
   let fun boolf [] = false