# HG changeset patch
# User wenzelm
# Date 1430406050 -7200
# Node ID d72795f401c35284f8b413ac2646311e3f8e1399
# Parent  81a0900f0ddceb020c642448cb596f878432677c
avoid potential conflict with Eisbach keyword (although keywords are local to the theory context);

diff -r 81a0900f0ddc -r d72795f401c3 src/ZF/AC/AC16_WO4.thy
--- a/src/ZF/AC/AC16_WO4.thy	Tue Apr 28 13:30:28 2015 +0200
+++ b/src/ZF/AC/AC16_WO4.thy	Thu Apr 30 17:00:50 2015 +0200
@@ -541,7 +541,7 @@
                                   THEN apply_type])+
 done
 
-lemma (in AC16) conclusion:
+lemma (in AC16) "conclusion":
      "\<exists>a f. Ord(a) & domain(f) = a & (\<Union>b<a. f ` b) = x & (\<forall>b<a. f ` b \<lesssim> m)"
 apply (rule well_ord_LL [THEN exE])
 apply (rename_tac S)