diff -r 5eb932e604a2 -r eab6ce8368fa 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)