--- a/Nominal/Perm.thy	Mon May 24 20:02:37 2010 +0100
+++ b/Nominal/Perm.thy	Mon May 24 20:50:15 2010 +0100
@@ -2,58 +2,23 @@
 imports 
   "../Nominal-General/Nominal2_Base"
   "../Nominal-General/Nominal2_Atoms" 
-  "Nominal2_FSet"
+  "Nominal2_FSet" "Abs"
 uses ("nominal_dt_rawperm.ML")
      ("nominal_dt_rawfuns.ML")
+     ("nominal_dt_alpha.ML")
 begin
 
 use "nominal_dt_rawperm.ML"
-use "nominal_dt_rawfuns.ML"
-
-ML {*
-open Nominal_Dt_RawPerm
-open Nominal_Dt_RawFuns
-*}
+ML {* open Nominal_Dt_RawPerm *}
 
-ML {*
-fun is_atom ctxt ty =
-  Sign.of_sort (ProofContext.theory_of ctxt) (ty, @{sort at_base})
-
-fun is_atom_set ctxt (Type ("fun", [t, @{typ bool}])) = is_atom ctxt t
-  | is_atom_set _ _ = false;
-
-fun is_atom_fset ctxt (Type (@{type_name "fset"}, [t])) = is_atom ctxt t
-  | is_atom_fset _ _ = false;
-
-fun is_atom_list ctxt (Type (@{type_name "list"}, [t])) = is_atom ctxt t
-  | is_atom_list _ _ = false
-
+use "nominal_dt_rawfuns.ML"
+ML {* open Nominal_Dt_RawFuns *}
 
-(* functions for producing sets, fsets and lists of general atom type
-   out from concrete atom types *)
-fun mk_atom_set t =
-let
-  val ty = fastype_of t;
-  val atom_ty = HOLogic.dest_setT ty --> @{typ "atom"};
-  val img_ty = atom_ty --> ty --> @{typ "atom set"};
-in
-  Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t
-end
+use "nominal_dt_alpha.ML"
+ML {* open Nominal_Dt_Alpha *}
 
-fun mk_atom_fset t =
-let
-  val ty = fastype_of t;
-  val atom_ty = dest_fsetT ty --> @{typ "atom"};
-  val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
-  val fset_to_set = @{term "fset_to_set :: atom fset => atom set"}
-in
-  fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t)
-end
-*}
 (* permutations for quotient types *)
 
-ML {* Class_Target.prove_instantiation_exit_result *}
-
 ML {*
 fun quotient_lift_consts_export qtys spec ctxt =
 let
@@ -112,31 +77,4 @@
 end
 *}
 
-
-
-(* Test *)
-(*
-atom_decl name
-
-datatype trm =
-  Var "name"
-| App "trm" "(trm list) list"
-| Lam "name" "trm"
-| Let "bp" "trm" "trm"
-and bp =
-  BUnit
-| BVar "name"
-| BPair "bp" "bp"
-
-setup {* fn thy =>
-let 
-  val info = Datatype.the_info thy "Perm.trm"
-in
-  define_raw_perms info 2 thy |> snd
 end
-*}
-
-print_theorems
-*)
-
-end