diff -r 5eb932e604a2 -r eab6ce8368fa src/HOL/Types_To_Sets/Examples/Finite.thy
--- a/src/HOL/Types_To_Sets/Examples/Finite.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Types_To_Sets/Examples/Finite.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -33,7 +33,7 @@
   includes lifting_syntax
   assumes [transfer_rule]: "right_total T"
   assumes [transfer_rule]: "bi_unique T"
-  shows "((T ===> op =) ===> op=) (injective_on (Collect(Domainp T))) injective"
+  shows "((T ===> (=)) ===> (=)) (injective_on (Collect(Domainp T))) injective"
   unfolding injective_on_def[abs_def] injective_def[abs_def] by transfer_prover
 
 text\<open>Similarly, we define the relativization of the internalization
@@ -44,7 +44,7 @@
 lemma class_finite_transfer[transfer_rule]:
   assumes [transfer_rule]: "right_total (T::'a\<Rightarrow>'b\<Rightarrow>bool)"
   assumes [transfer_rule]: "bi_unique T"
-  shows "op= (finite_on (Collect(Domainp T))) (class.finite TYPE('b))"
+  shows "(=) (finite_on (Collect(Domainp T))) (class.finite TYPE('b))"
   unfolding finite_on_def class.finite_def by transfer_prover
 
 text\<open>The aforementioned development can be automated. The main part is already automated