updated to new Isabelle
authorChristian Urban <urbanc@in.tum.de>
Sat, 28 Aug 2010 13:41:31 +0800
changeset 2446 63c936b09764
parent 2445 10148a447359
child 2447 76be909eaf04
updated to new Isabelle
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)