proper use of "member", without embarking on delicate questions about SML equality types;
authorwenzelm
Thu, 14 Mar 2013 13:57:44 +0100
changeset 51427 08bb00239652
parent 51426 f25ee4fb437d
child 51428 12e46440e391
proper use of "member", without embarking on delicate questions about SML equality types;
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."