Updated comment about list_subset_univ and list_into_univ.

--- a/src/ZF/List.ML	Mon Feb 27 17:27:50 1995 +0100
+++ b/src/ZF/List.ML	Mon Feb 27 17:40:57 1995 +0100
@@ -46,7 +46,7 @@
 			    Pair_in_univ]) 1);
 qed "list_univ";
 
-(*These two theorems are unused -- useful??*)
+(*These two theorems justify datatypes involving list(nat), list(A), ...*)
 bind_thm ("list_subset_univ", ([list_mono, list_univ] MRS subset_trans));
 
 goal List.thy "!!l A B. [| l: list(A);  A <= univ(B) |] ==> l: univ(B)";