--- a/Nominal-General/nominal_atoms.ML	Tue Apr 27 19:51:35 2010 +0200
+++ b/Nominal-General/nominal_atoms.ML	Tue Apr 27 22:21:16 2010 +0200
@@ -15,24 +15,13 @@
 structure Atom_Decl :> ATOM_DECL =
 struct
 
-val atomT = @{typ atom};
-val permT = @{typ perm};
-
-val sort_of_const = @{term sort_of};
-fun atom_const T = Const (@{const_name atom}, T --> atomT);
-fun permute_const T = Const (@{const_name permute}, permT --> T --> T);
-
-fun mk_sort_of t = sort_of_const $ t;
-fun mk_atom t = atom_const (fastype_of t) $ t;
-fun mk_permute (p, t) = permute_const (fastype_of t) $ p $ t;
-
 fun atom_decl_set (str : string) : term =
   let
-    val a = Free ("a", atomT);
+    val a = Free ("a", @{typ atom});
     val s = Const (@{const_name "Sort"}, @{typ "string => atom_sort list => atom_sort"})
               $ HOLogic.mk_string str $ HOLogic.nil_const @{typ "atom_sort"};
   in
-    HOLogic.mk_Collect ("a", atomT, HOLogic.mk_eq (mk_sort_of a, s))
+    HOLogic.mk_Collect ("a", @{typ atom}, HOLogic.mk_eq (mk_sort_of a, s))
   end
 
 fun add_atom_decl (name : binding, arg : binding option) (thy : theory) =
@@ -48,15 +37,15 @@
 
     (* definition of atom and permute *)
     val newT = #abs_type (fst info);
-    val RepC = Const (Rep_name, newT --> atomT);
-    val AbsC = Const (Abs_name, atomT --> newT);
+    val RepC = Const (Rep_name, newT --> @{typ atom});
+    val AbsC = Const (Abs_name, @{typ atom} --> newT);
     val a = Free ("a", newT);
-    val p = Free ("p", permT);
+    val p = Free ("p", @{typ perm});
     val atom_eqn =
       HOLogic.mk_Trueprop (HOLogic.mk_eq (mk_atom a, RepC $ a));
     val permute_eqn =
       HOLogic.mk_Trueprop (HOLogic.mk_eq
-        (mk_permute (p, a), AbsC $ (mk_permute (p, RepC $ a))));
+        (mk_perm p a, AbsC $ (mk_perm p (RepC $ a))));
     val atom_def_name =
       Binding.prefix_name "atom_" (Binding.suffix_name "_def" name);
     val permute_def_name =