src/HOL/Nominal/nominal_atoms.ML
changeset 23029 79ee75dc1e59
parent 22846 fb79144af9a3
child 23158 749b6870b1a1
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat May 19 11:33:34 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat May 19 11:33:57 2007 +0200
     1.3 @@ -204,7 +204,7 @@
     1.4            val pi2 = Free ("pi2", mk_permT T);
     1.5            val cperm = Const ("Nominal.perm", mk_permT T --> ty --> ty);
     1.6            val cnil  = Const ("List.list.Nil", mk_permT T);
     1.7 -          val cappend = Const ("List.op @",mk_permT T --> mk_permT T --> mk_permT T);
     1.8 +          val cappend = Const ("List.append",mk_permT T --> mk_permT T --> mk_permT T);
     1.9            val cprm_eq = Const ("Nominal.prm_eq",mk_permT T --> mk_permT T --> HOLogic.boolT);
    1.10            (* nil axiom *)
    1.11            val axiom1 = HOLogic.mk_Trueprop (HOLogic.mk_eq