| changeset 67399 | eab6ce8368fa |
| parent 67386 | 998e01d6f8fd |
| child 67463 | a5ca98950a91 |
--- a/src/HOL/Library/LaTeXsugar.thy Wed Jan 10 15:21:49 2018 +0100 +++ b/src/HOL/Library/LaTeXsugar.thy Wed Jan 10 15:25:09 2018 +0100 @@ -118,7 +118,7 @@ let val rhs_vars = Term.add_vars rhs []; fun dummy (v as Var (ixn as (_, T))) = - if member (op = ) rhs_vars ixn then v else Const (@{const_name DUMMY}, T) + if member ((=) ) rhs_vars ixn then v else Const (@{const_name DUMMY}, T) | dummy (t $ u) = dummy t $ dummy u | dummy (Abs (n, T, b)) = Abs (n, T, dummy b) | dummy t = t;