src/HOL/Nominal/nominal_atoms.ML
changeset 22846 fb79144af9a3
parent 22794 d0f483fd57dd
child 23029 79ee75dc1e59
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sun May 06 21:50:17 2007 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Mon May 07 00:49:59 2007 +0200
     1.3 @@ -13,7 +13,6 @@
     1.4    val get_atom_info : theory -> string -> atom_info option
     1.5    val atoms_of : theory -> string list
     1.6    val mk_permT : typ -> typ
     1.7 -  val setup : theory -> theory
     1.8  end
     1.9  
    1.10  structure NominalAtoms : NOMINAL_ATOMS =
    1.11 @@ -23,27 +22,21 @@
    1.12  val Collect_const = thm "Collect_const";
    1.13  
    1.14  
    1.15 -(* data kind 'HOL/nominal' *)
    1.16 +(* theory data *)
    1.17  
    1.18  type atom_info =
    1.19    {pt_class : string,
    1.20     fs_class : string,
    1.21     cp_classes : (string * string) list};
    1.22  
    1.23 -structure NominalArgs =
    1.24 -struct
    1.25 -  val name = "HOL/nominal";
    1.26 +structure NominalData = TheoryDataFun
    1.27 +(
    1.28    type T = atom_info Symtab.table;
    1.29 -
    1.30    val empty = Symtab.empty;
    1.31    val copy = I;
    1.32    val extend = I;
    1.33    fun merge _ x = Symtab.merge (K true) x;
    1.34 -
    1.35 -  fun print sg tab = ();
    1.36 -end;
    1.37 -
    1.38 -structure NominalData = TheoryDataFun(NominalArgs);
    1.39 +);
    1.40  
    1.41  fun make_atom_info ((pt_class, fs_class), cp_classes) =
    1.42    {pt_class = pt_class,
    1.43 @@ -889,6 +882,4 @@
    1.44  
    1.45  val _ = OuterSyntax.add_parsers [atom_declP];
    1.46  
    1.47 -val setup = NominalData.init;
    1.48 -
    1.49  end;