diff -r 13d93ac68b07 -r f2d4dae2a10b Nominal-General/nominal_library.ML
--- a/Nominal-General/nominal_library.ML	Thu Aug 19 16:08:10 2010 +0900
+++ b/Nominal-General/nominal_library.ML	Thu Aug 19 18:24:36 2010 +0800
@@ -276,13 +276,13 @@
  R ... /\ P ...; split_conj_i picks out
  the part R or P part
 *)
-fun split_conj1 names (Const ("op &", _) $ f1 $ f2) = 
+fun split_conj1 names (Const (@{const_name "op &"}, _) $ 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 ("op &", _) $ f1 $ f2) = 
+fun split_conj2 names (Const (@{const_name "op &"}, _) $ f1 $ f2) = 
   (case head_of f1 of
      Const (name, _) => if member (op =) names name then SOME f2 else NONE
    | _ => NONE)