avoid potential conflict with Eisbach keyword (although keywords are local to the theory context);

--- 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)