src/HOL/Nominal/nominal_atoms.ML
changeset 18746 a4ece70964ae
parent 18707 9d6154f76476
child 18759 2f55e3e47355
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sun Jan 22 21:58:43 2006 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sun Jan 22 22:11:50 2006 +0100
     1.3 @@ -5,7 +5,7 @@
     1.4    val create_nom_typedecls : string list -> theory -> theory
     1.5    val atoms_of : theory -> string list
     1.6    val mk_permT : typ -> typ
     1.7 -  val setup : (theory -> theory) list
     1.8 +  val setup : theory -> theory
     1.9  end
    1.10  
    1.11  structure NominalAtoms : NOMINAL_ATOMS =
    1.12 @@ -784,6 +784,6 @@
    1.13  
    1.14  val _ = OuterSyntax.add_parsers [atom_declP];
    1.15  
    1.16 -val setup = [NominalData.init];
    1.17 +val setup = NominalData.init;
    1.18  
    1.19  end;