# HG changeset patch
# User paulson
# Date 849180991 -3600
# Node ID 7c4744ed8fc3d8dc05af8fbdaee8ab333a684be4
# Parent  d7513875b2b89857dc72d67e74230db740033ffa
Declares List_ as a synonym for List

diff -r d7513875b2b8 -r 7c4744ed8fc3 src/Pure/library.ML
--- 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