--- a/Nominal/NewFv.thy	Tue Apr 27 22:21:16 2010 +0200
+++ b/Nominal/NewFv.thy	Tue Apr 27 22:45:50 2010 +0200
@@ -15,6 +15,7 @@
   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
 
   fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom x];
+
   val noatoms = @{term "{} :: atom set"};
   fun mk_union sets =
     fold (fn a => fn b =>
@@ -25,8 +26,8 @@
 *}
 
 ML {*
-fun is_atom thy typ =
-  Sign.of_sort thy (typ, @{sort at})
+fun is_atom thy ty =
+  Sign.of_sort thy (ty, @{sort at})
 
 fun is_atom_set thy (Type ("fun", [t, @{typ bool}])) = is_atom thy t
   | is_atom_set _ _ = false;
@@ -40,7 +41,7 @@
   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) $ Const (@{const_name atom}, atom_ty) $ t)
+  (Const (@{const_name image}, img_ty) $ mk_atom_ty atom_ty t)
 end;
 
 fun mk_atom_fset t =
@@ -50,7 +51,7 @@
   val fmap_ty = atom_ty --> ty --> @{typ "atom fset"};
   val fset_to_set = @{term "fset_to_set :: atom fset \<Rightarrow> atom set"}
 in
-  fset_to_set $ ((Const (@{const_name fmap}, fmap_ty) $ Const (@{const_name atom}, atom_ty) $ t))
+  fset_to_set $ (Const (@{const_name fmap}, fmap_ty) $ mk_atom_ty atom_ty t)
 end;
 
 fun mk_diff a b =
@@ -60,21 +61,25 @@
 *}
 
 ML {*
-fun atoms thy x =
+fun atoms thy t =
 let
-  val ty = fastype_of x;
+  val ty = fastype_of t;
 in
-  if is_atom thy ty then mk_single_atom x else
-  if is_atom_set thy ty then mk_atom_set x else
-  if is_atom_fset thy ty then mk_atom_fset x else
-  @{term "{} :: atom set"}
+  if is_atom thy ty 
+    then mk_single_atom t 
+  else if is_atom_set thy ty 
+    then mk_atom_set t 
+  else if is_atom_fset thy ty 
+    then mk_atom_fset t 
+  else noatoms
 end
 *}
 
 ML {*
 fun setify x =
-  if fastype_of x = @{typ "atom list"} then
-  Const (@{const_name set}, @{typ "atom list \<Rightarrow> atom set"}) $ x else x
+  if fastype_of x = @{typ "atom list"} 
+    then @{term "set::atom list \<Rightarrow> atom set"} $ x 
+    else x
 *}
 
 ML {*
@@ -199,6 +204,7 @@
   map2 fv_constr constrs bmll
 end
 *}
+
 ML {*
 val by_pat_completeness_auto =
   Proof.global_terminal_proof
@@ -213,7 +219,7 @@
 
 
 ML {*
-fun define_fv dt_info bns bmlll lthy =
+fun define_raw_fv dt_info bns bmlll lthy =
 let
   val thy = ProofContext.theory_of lthy;
   val {descr, sorts, ...} = dt_info;