# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273147761 -7200
# Node ID 2b6ba4d4e19ae5f6545a47181891af7ee0466807
# Parent  79b733010bc5dc03d4cf30ae06830d3415e5c928
Fixes for new isabelle

diff -r 79b733010bc5 -r 2b6ba4d4e19a Nominal-General/nominal_eqvt.ML
--- a/Nominal-General/nominal_eqvt.ML	Thu May 06 13:25:37 2010 +0200
+++ b/Nominal-General/nominal_eqvt.ML	Thu May 06 14:09:21 2010 +0200
@@ -77,7 +77,7 @@
 let
   fun split_conj names (Const ("op &", _) $ f1 $ f2) = 
       (case head_of f1 of
-         Const (name, _) => if name mem names then SOME f2 else NONE
+         Const (name, _) => if member (op =) names name then SOME f2 else NONE
        | _ => NONE)
   | split_conj _ _ = NONE;
 in
@@ -178,4 +178,4 @@
       K.thy_decl (P.xname >> equivariance);
 end;
 
-end (* structure *)
\ No newline at end of file
+end (* structure *)
diff -r 79b733010bc5 -r 2b6ba4d4e19a Nominal-General/nominal_permeq.ML
--- a/Nominal-General/nominal_permeq.ML	Thu May 06 13:25:37 2010 +0200
+++ b/Nominal-General/nominal_permeq.ML	Thu May 06 14:09:21 2010 +0200
@@ -117,7 +117,7 @@
     let
       val hd = head_of trm
     in 
-      if is_Const hd andalso (fst (dest_Const hd)) mem bad_hds then ()
+      if is_Const hd andalso member (op =) bad_hds (fst (dest_Const hd)) then ()
       else (if strict_flag then error else warning) 
              ("Cannot solve equivariance for " ^ (Syntax.string_of_term ctxt trm))
     end
@@ -183,4 +183,4 @@
 fun perm_strict_simp_meth (thms, consts) ctxt = 
   SIMPLE_METHOD (HEADGOAL (eqvt_strict_tac ctxt thms consts))
 
-end; (* structure *)
\ No newline at end of file
+end; (* structure *)