--- 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)