# HG changeset patch
# User wenzelm
# Date 1363265864 -3600
# Node ID 08bb002396528f988f2028e50a1a772105701d3c
# Parent  f25ee4fb437d851c3fd7a5ecd6eaa5f48bd02375
proper use of "member", without embarking on delicate questions about SML equality types;

diff -r f25ee4fb437d -r 08bb00239652 src/HOL/Tools/Lifting/lifting_info.ML
--- a/src/HOL/Tools/Lifting/lifting_info.ML	Thu Mar 14 13:52:22 2013 +0100
+++ b/src/HOL/Tools/Lifting/lifting_info.ML	Thu Mar 14 13:57:44 2013 +0100
@@ -247,12 +247,10 @@
     val _ = if has_duplicates op= concl_pairs 
       then error "The rule contains duplicated variables in the conlusion." else ()
 
-    fun mem a l = member op= l a
-
     fun rewrite_prem prem_pair = 
-      if mem prem_pair concl_pairs 
+      if member op= concl_pairs prem_pair
       then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm POS_def}))
-      else if mem (swap prem_pair) concl_pairs 
+      else if member op= concl_pairs (swap prem_pair)
         then HOLogic.Trueprop_conv (Conv.rewr_conv (Thm.symmetric @{thm NEG_def}))
       else error "The rule contains a non-relevant assumption."