src/HOL/Nominal/nominal_atoms.ML

 end
 
 structure NominalAtoms : NOMINAL_ATOMS =
 struct
 
-val Finites_emptyI = thm "Finites.emptyI";
+val finite_emptyI = thm "finite.emptyI";
 val Collect_const = thm "Collect_const";
 
 
 (* data kind 'HOL/nominal' *)
 

     (* <ak>_infinite: infinite (UNIV::<ak_type> set) *)
     val (inf_axs,thy2) = PureThy.add_axioms_i (map (fn (ak_name, T) =>
       let 
     val name = ak_name ^ "_infinite"
         val axiom = HOLogic.mk_Trueprop (HOLogic.mk_not
-                    (HOLogic.mk_mem (HOLogic.mk_UNIV T,
-                     Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T)))))
+                    (Const ("Finite_Set.finite", HOLogic.mk_setT T --> HOLogic.boolT) $
+                       HOLogic.mk_UNIV T))
       in
         ((name, axiom), []) 
       end) ak_names_types) thy1;
     
     (* declares a swapping function for every atom-kind, it is         *)

 	  val cl_name = "fs_"^ak_name;
 	  val pt_name = Sign.full_name thy ("pt_"^ak_name);
           val ty = TFree("'a",["HOL.type"]);
           val x   = Free ("x", ty);
           val csupp    = Const ("Nominal.supp", ty --> HOLogic.mk_setT T);
-          val cfinites = Const ("Finite_Set.Finites", HOLogic.mk_setT (HOLogic.mk_setT T))
+          val cfinite  = Const ("Finite_Set.finite", HOLogic.mk_setT T --> HOLogic.boolT)
           
-          val axiom1   = HOLogic.mk_Trueprop (HOLogic.mk_mem (csupp $ x, cfinites));
+          val axiom1   = HOLogic.mk_Trueprop (cfinite $ (csupp $ x));
 
        in  
         AxClass.define_class_i (cl_name, [pt_name]) [] [((cl_name ^ "1", []), [axiom1])] thy            
        end) ak_names_types thy8; 
 

                   let val at_thm = PureThy.get_thm thy' (Name ("at_"^ak_name^"_inst"));
                   in  EVERY [ClassPackage.intro_classes_tac [],
                              rtac ((at_thm RS fs_at_inst) RS fs1) 1] end
                 else
                   let val dj_inst = PureThy.get_thm thy' (Name ("dj_"^ak_name'^"_"^ak_name));
-                      val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, Finites_emptyI];
+                      val simp_s = HOL_basic_ss addsimps [dj_inst RS dj_supp, finite_emptyI];
                   in EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1] end)
         in
          AxClass.prove_arity (qu_name,[],[qu_class]) proof thy'
         end) ak_names thy) ak_names thy18;
 

           fun discrete_fs_inst discrete_ty defn = 
 	     fold (fn ak_name => fn thy =>
 	     let
 	       val qu_class = Sign.full_name thy ("fs_"^ak_name);
 	       val supp_def = thm "Nominal.supp_def";
-               val simp_s = HOL_ss addsimps [supp_def,Collect_const,Finites_emptyI,defn];
+               val simp_s = HOL_ss addsimps [supp_def,Collect_const,finite_emptyI,defn];
                val proof = EVERY [ClassPackage.intro_classes_tac [], asm_simp_tac simp_s 1];
              in 
 	       AxClass.prove_arity (discrete_ty,[],[qu_class]) proof thy
              end) ak_names;