diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/BNF_Wellorder_Embedding.thy
--- a/src/HOL/BNF_Wellorder_Embedding.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/BNF_Wellorder_Embedding.thy	Fri May 13 20:24:10 2016 +0200
@@ -986,7 +986,7 @@
 
 lemma iso_Field:
 "iso r r' f \<Longrightarrow> f ` (Field r) = Field r'"
-using assms by (auto simp add: iso_def bij_betw_def)
+by (auto simp add: iso_def bij_betw_def)
 
 lemma iso_iff:
 assumes "Well_order r"