src/HOL/MicroJava/BV/Typing_Framework_JVM.thy

--- a/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/MicroJava/BV/Typing_Framework_JVM.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -182,7 +182,7 @@
   by (induct n, auto)
 
 lemma lesubstep_type_simple:
-  "a <=[Product.le (op =) r] b \<Longrightarrow> a \<le>|r| b"
+  "a <=[Product.le (=) r] b \<Longrightarrow> a \<le>|r| b"
   apply (unfold lesubstep_type_def)
   apply clarify
   apply (simp add: set_conv_nth)