--- a/src/HOL/Library/Pattern_Aliases.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Library/Pattern_Aliases.thy Wed Jan 10 15:25:09 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 op = (x, t) | _ => I) t []
+ fold_aterms (fn Free (x, t) => insert (=) (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 op = vars) (all_Frees res)
+ val frees = filter (member (=) vars) (all_Frees res)
in fold (fn v => Logic.dependent_all_name ("", v)) (map Free frees) res end
| _ => t
@@ -207,4 +207,4 @@
end
-end
\ No newline at end of file
+end