diff -r e128ab544996 -r e9ab4ad7bd15 src/HOL/Library/Pattern_Aliases.thy
--- a/src/HOL/Library/Pattern_Aliases.thy	Thu Jan 11 12:32:07 2018 +0100
+++ b/src/HOL/Library/Pattern_Aliases.thy	Thu Jan 11 13:48:17 2018 +0100
@@ -60,7 +60,7 @@
   | SOME (var, t) => apfst (cons var) (strip_all t)
 
 fun all_Frees t =
-  fold_aterms (fn Free (x, t) => insert (=) (x, t) | _ => I) t []
+  fold_aterms (fn Free (x, t) => insert (op =) (x, t) | _ => I) t []
 
 fun subst_once (old, new) t =
   let
@@ -120,7 +120,7 @@
 
         val res = HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs', rhs'))
 
-        val frees = filter (member (=) vars) (all_Frees res)
+        val frees = filter (member (op =) vars) (all_Frees res)
       in fold (fn v => Logic.dependent_all_name ("", v)) (map Free frees) res end
   | _ => t