src/HOL/Library/LaTeXsugar.thy
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;