ZF/ex/LList/lconst_type: streamlined proof

--- a/src/ZF/ex/LList.ML	Tue Aug 23 19:34:01 1994 +0200
+++ b/src/ZF/ex/LList.ML	Wed Aug 24 15:48:47 1994 +0200
@@ -136,7 +136,7 @@
 
 goal LList.thy "!!a A. a:A ==> lconst(a): llist(A)";
 by (rtac (singletonI RS llist.coinduct) 1);
-by (fast_tac (ZF_cs addSIs [lconst_in_quniv]) 1);
+by (etac (lconst_in_quniv RS singleton_subsetI) 1);
 by (fast_tac (ZF_cs addSIs [lconst]) 1);
 val lconst_type = result();