diff -r 888bbb4119f8 -r 89e1986125fe src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Fri Jun 17 17:49:03 1994 +0200
+++ b/src/HOLCF/Fix.ML	Mon Jun 20 12:03:16 1994 +0200
@@ -1072,6 +1072,27 @@
 	(atac 1)
 	]);
 
+
+val adm_disj_lemma11 = prove_goal Fix.thy
+"[| adm(P); is_chain(Y); ! i. ? j. i < j & P(Y(j)) |]==>P(lub(range(Y)))"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac adm_disj_lemma2 1),
+	(etac adm_disj_lemma10 1),
+	(atac 1)
+	]);
+
+val adm_disj_lemma12 = prove_goal Fix.thy
+"[| adm(P); is_chain(Y);? i. ! j. i < j --> P(Y(j))|]==>P(lub(range(Y)))"
+ (fn prems =>
+	[
+	(cut_facts_tac prems 1),
+	(etac adm_disj_lemma2 1),
+	(etac adm_disj_lemma6 1),
+	(atac 1)
+	]);
+
 val adm_disj = prove_goal  Fix.thy  
 	"[| adm(P); adm(Q) |] ==> adm(%x.P(x)|Q(x))"
  (fn prems =>
@@ -1083,19 +1104,16 @@
 	(atac 1),
 	(atac 1),
 	(rtac disjI2 1),
-	(rtac adm_disj_lemma2 1),
-	(atac 1),
-	(rtac adm_disj_lemma6 1),
+	(etac adm_disj_lemma12 1),
 	(atac 1),
 	(atac 1),
 	(rtac disjI1 1),
-	(rtac adm_disj_lemma2 1),
-	(atac 1),
-	(rtac adm_disj_lemma10 1),
+	(etac adm_disj_lemma11 1),
 	(atac 1),
 	(atac 1)
 	]);
 
+
 val adm_impl = prove_goal  Fix.thy  
 	"[| adm(%x.~P(x)); adm(Q) |] ==> adm(%x.P(x)-->Q(x))"
  (fn prems =>