# HG changeset patch
# User lcp
# Date 777736127 -7200
# Node ID 46927979041080968834b5a38c1270d1b2e4a30b
# Parent  74f0e5fce609fb66ce6f8fdf6d213dbf46400e99
ZF/ex/LList/lconst_type: streamlined proof

diff -r 74f0e5fce609 -r 469279790410 src/ZF/ex/LList.ML
--- 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();