diff -r 1a20fd9cf281 -r eb4ddd18d635 src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy
--- a/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Hahn_Banach/Hahn_Banach_Sup_Lemmas.thy	Mon Apr 25 16:09:26 2016 +0200
@@ -158,7 +158,7 @@
 \<close>
 
 lemma sup_definite:
-  assumes M_def: "M \<equiv> norm_pres_extensions E p F f"
+  assumes M_def: "M = norm_pres_extensions E p F f"
     and cM: "c \<in> chains M"
     and xy: "(x, y) \<in> \<Union>c"
     and xz: "(x, z) \<in> \<Union>c"