src/HOL/NSA/NSComplex.thy

--- a/src/HOL/NSA/NSComplex.thy	Wed Dec 30 17:45:18 2015 +0100
+++ b/src/HOL/NSA/NSComplex.thy	Wed Dec 30 17:55:43 2015 +0100
@@ -206,7 +206,7 @@
 by transfer (rule Im_complex_of_real)
 
 lemma hcomplex_of_hypreal_epsilon_not_zero [simp]:
-     "hcomplex_of_hypreal epsilon \<noteq> 0"
+     "hcomplex_of_hypreal \<epsilon> \<noteq> 0"
 by (simp add: hypreal_epsilon_not_zero)
 
 subsection\<open>HComplex theorems\<close>