diff -r bf748be70109 -r c148a6ea784e Nominal/nominal_dt_rawfuns.ML
--- a/Nominal/nominal_dt_rawfuns.ML	Thu May 20 21:35:00 2010 +0100
+++ b/Nominal/nominal_dt_rawfuns.ML	Thu May 20 21:47:12 2010 +0100
@@ -47,7 +47,7 @@
 fun mk_atom_set t =
 let
   val ty = fastype_of t;
-  val atom_ty = HOLogic.dest_setT ty --> @{typ atom};
+  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)
@@ -56,13 +56,14 @@
 fun mk_atom_fset t =
 let
   val ty = fastype_of t;
-  val atom_ty = dest_fsetT ty --> @{typ atom};
+  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;
 
+(*
 fun mk_atom_list t =
 let
   val ty = fastype_of t;
@@ -71,7 +72,7 @@
 in
   (Const (@{const_name map}, map_ty) $ mk_atom_ty atom_ty t)
 end;
-
+*)
 
 (* functions that coerces atoms, sets and fsets into atom sets ? *)
 fun setify ctxt t =
@@ -100,14 +101,15 @@
 end
 
 (* coerces a list into a set *)
-fun to_set x =
-  if fastype_of x = @{typ "atom list"}
-  then @{term "set::atom list => atom set"} $ x
-  else x
+fun to_set t =
+  if fastype_of t = @{typ "atom list"}
+  then @{term "set::atom list => atom set"} $ t
+  else t
 
 
+(* functions that construct the equations for fv and fv_bn *)
 
-fun make_body fv_map args i = 
+fun make_fv_body fv_map args i = 
 let
   val arg = nth args i
   val ty = fastype_of arg
@@ -117,7 +119,7 @@
   | SOME fv => fv $ arg
 end  
 
-fun make_binder lthy fv_bn_map args (bn_option, i) = 
+fun make_fv_binder lthy fv_bn_map args (bn_option, i) = 
 let
   val arg = nth args i
 in
@@ -128,8 +130,8 @@
 
 fun make_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) =
 let
-  val t1 = map (make_body fv_map args) bodies
-  val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders)
+  val t1 = map (make_fv_body fv_map args) bodies
+  val (t2, t3) = split_list (map (make_fv_binder lthy fv_bn_map args) binders)
 in 
   fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
 end
@@ -147,7 +149,7 @@
 end
 
 
-fun make_bn_body fv_map fv_bn_map bn_args args i = 
+fun make_fv_bn_body fv_map fv_bn_map bn_args args i = 
 let
   val arg = nth args i
   val ty = fastype_of arg
@@ -162,16 +164,16 @@
 
 fun make_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause =
   case bclause of
-    BC (_, [], bodies) => fold_union (map (make_bn_body fv_map fv_bn_map bn_args args) bodies)
+    BC (_, [], bodies) => fold_union (map (make_fv_bn_body fv_map fv_bn_map bn_args args) bodies)
   | BC (_, binders, bodies) => 
       let
-        val t1 = map (make_body fv_map args) bodies
-        val (t2, t3) = split_list (map (make_binder lthy fv_bn_map args) binders)
+        val t1 = map (make_fv_body fv_map args) bodies
+        val (t2, t3) = split_list (map (make_fv_binder lthy fv_bn_map args) binders)
       in 
         fold_union (mk_diff (fold_union t1, fold_union t2)::t3)
       end
 
-fun make_fv_bn_eq lthy bn_trm fv_map fv_bn_map (bn_args, (constr, ty, arg_tys)) bclauses =
+fun make_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)