--- a/src/HOL/Nominal/nominal_atoms.ML Sat May 19 11:33:34 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Sat May 19 11:33:57 2007 +0200
@@ -204,7 +204,7 @@
val pi2 = Free ("pi2", mk_permT T);
val cperm = Const ("Nominal.perm", mk_permT T --> ty --> ty);
val cnil = Const ("List.list.Nil", mk_permT T);
- val cappend = Const ("List.op @",mk_permT T --> mk_permT T --> mk_permT T);
+ val cappend = Const ("List.append",mk_permT T --> mk_permT T --> mk_permT T);
val cprm_eq = Const ("Nominal.prm_eq",mk_permT T --> mk_permT T --> HOLogic.boolT);
(* nil axiom *)
val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq