--- a/Quot/Nominal/Fv.thy	Wed Feb 17 14:35:06 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Wed Feb 17 14:44:32 2010 +0100
@@ -39,8 +39,6 @@
  [[], [], [(SOME (Const f), 0), (Some (Const g), 1)]]]
 *)
 
-ML foldr1
-ML fold
 ML {*
   val {descr, ...} = Datatype.the_info @{theory} "Fv.rlam";
   val sorts = [];
@@ -51,6 +49,7 @@
     "fv_" ^ name_of_typ (nth_dtyp i)) descr);
   val fv_types = map (fn (i, _) => nth_dtyp i --> @{typ "atom set"}) descr;
   val fv_frees = map Free (fv_names ~~ fv_types);
+  fun mk_single_atom x = HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x]
   fun mk_union sets =
     fold (fn a => fn b =>
       if a = noatoms then b else
@@ -58,7 +57,7 @@
       HOLogic.mk_binop @{const_name union} (a, b)) sets noatoms;
   fun mk_diff a b =
     if b = noatoms then a else
-    HOLogic.mk_binop @{const_name "Algebras.minus_class.minus"} (a, b);
+    HOLogic.mk_binop @{const_name minus} (a, b);
   fun fv_eq_constr i (cname, dts) bindcs =
     let
       val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -66,12 +65,14 @@
       val args = map Free (names ~~ Ts);
       val c = Const (cname, Ts ---> (nth_dtyp i));
       val fv_c = Free (nth fv_names i, (nth_dtyp i) --> @{typ "atom set"});
-      fun fv_bind (_, i) = @{term "{} :: atom set"}
+      (* TODO we assume that all can be 'atomized' *)
+      fun fv_bind (NONE, i) = mk_single_atom (nth args i)
+        | fv_bind (SOME f, i) = f $ (nth args i);
       fun fv_arg ((dt, x), bindxs) =
         let
           val arg =
             if is_rec_type dt then nth fv_frees (body_index dt) $ x
-            (* TODO: we just assume everything is a 'name' *)
+            (* TODO: we just assume everything can be 'atomized' *)
             else HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x]
           val sub = mk_union (map fv_bind bindxs)
         in