# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1282974091 -28800
# Node ID 63c936b09764bbb01e56fafb7e25673c3bc9b2c3
# Parent  10148a447359824dcf29d0eebf2d5f3731eebc8c
updated to new Isabelle

diff -r 10148a447359 -r 63c936b09764 Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Fri Aug 27 23:26:00 2010 +0800
+++ b/Nominal-General/nominal_library.ML	Sat Aug 28 13:41:31 2010 +0800
@@ -276,13 +276,13 @@
  R ... /\ P ...; split_conj_i picks out
  the part R or P part
 *)
-fun split_conj1 names (Const (@{const_name "op &"}, _) $ f1 $ f2) = 
+fun split_conj1 names (Const (@{const_name "conj"}, _) $ f1 $ f2) = 
   (case head_of f1 of
      Const (name, _) => if member (op =) names name then SOME f1 else NONE
    | _ => NONE)
 | split_conj1 _ _ = NONE;
 
-fun split_conj2 names (Const (@{const_name "op &"}, _) $ f1 $ f2) = 
+fun split_conj2 names (Const (@{const_name "conj"}, _) $ f1 $ f2) = 
   (case head_of f1 of
      Const (name, _) => if member (op =) names name then SOME f2 else NONE
    | _ => NONE)