--- a/Nominal/nominal_dt_rawfuns.ML	Sun May 23 02:15:24 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Mon May 24 20:02:37 2010 +0100
@@ -15,6 +15,14 @@
   datatype bmode = Lst | Res | Set
   datatype bclause = BC of bmode * (term option * int) list * int list
 
+  val is_atom: Proof.context -> typ -> bool
+  val is_atom_set: Proof.context -> typ -> bool
+  val is_atom_fset: Proof.context -> typ -> bool
+  val is_atom_list: Proof.context -> typ -> bool
+  val mk_atom_set: term -> term
+  val mk_atom_fset: term -> term
+
+
   val setify: Proof.context -> term -> term
   val listify: Proof.context -> term -> term
 
@@ -151,7 +159,7 @@
     case AList.lookup (op=) bn_args i of
       NONE => (case (AList.lookup (op=) fv_map ty) of
                  NONE => mk_supp arg
-              | SOME fv => fv $ arg)
+               | SOME fv => fv $ arg)
     | SOME (NONE) => @{term "{}::atom set"}
     | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg
   end  
@@ -161,7 +169,7 @@
   | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause
 end
 
-fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = 
+fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys, _) bclauses = 
 let
   val arg_names = Datatype_Prop.make_tnames arg_tys
   val args = map Free (arg_names ~~ arg_tys)
@@ -173,7 +181,7 @@
   HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs))
 end
 
-fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys)) bclauses =
+fun mk_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, _, arg_tys, _)) bclauses =
 let
   val arg_names = Datatype_Prop.make_tnames arg_tys
   val args = map Free (arg_names ~~ arg_tys)
@@ -196,7 +204,7 @@
 fun define_raw_fvs descr sorts bn_info bclausesss lthy =
 let
   val fv_names = prefix_dt_names descr sorts "fv_"
-  val fv_arg_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr;
+  val fv_arg_tys = all_dtyps descr sorts
   val fv_tys = map (fn ty => ty --> @{typ "atom set"}) fv_arg_tys;
   val fv_frees = map Free (fv_names ~~ fv_tys);
   val fv_map = fv_arg_tys ~~ fv_frees