--- a/src/HOL/Quotient_Examples/Lift_FSet.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Wed Jan 10 15:25:09 2018 +0100
@@ -30,7 +30,7 @@
lemma list_eq_transfer [transfer_rule]:
assumes [transfer_rule]: "bi_unique A"
- shows "(list_all2 A ===> list_all2 A ===> op =) list_eq list_eq"
+ shows "(list_all2 A ===> list_all2 A ===> (=)) list_eq list_eq"
unfolding list_eq_def [abs_def] by transfer_prover
quotient_type 'a fset = "'a list" / "list_eq" parametric list_eq_transfer
@@ -90,7 +90,7 @@
lemma member_transfer:
assumes [transfer_rule]: "bi_unique A"
- shows "(A ===> list_all2 A ===> op=) (\<lambda>x xs. x \<in> set xs) (\<lambda>x xs. x \<in> set xs)"
+ shows "(A ===> list_all2 A ===> (=)) (\<lambda>x xs. x \<in> set xs) (\<lambda>x xs. x \<in> set xs)"
by transfer_prover
end