src/HOL/Bali/State.thy

--- a/src/HOL/Bali/State.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Bali/State.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -604,7 +604,7 @@
 apply clarify
 done
 
-lemma state_not_single: "All (op = (x::state)) \<Longrightarrow> R"
+lemma state_not_single: "All ((=) (x::state)) \<Longrightarrow> R"
 apply (drule_tac x = "(if abrupt x = None then Some x' else None, y)" for x' y in spec)
 apply clarsimp
 done