--- a/Quot/Nominal/Fv.thy	Wed Feb 17 14:44:32 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Wed Feb 17 15:00:04 2010 +0100
@@ -2,20 +2,6 @@
 imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs"
 begin
 
-atom_decl name
-
-datatype rlam =
-  rVar "name"
-| rApp "rlam" "rlam"
-| rLam "name" "rlam"
-
-ML {*
-  open Datatype_Aux (* typ_of_dtyp, DtRec, ... *);
-  fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom})
-*}
-
-ML {* dest_Type @{typ rlam} *}
-
 (* Bindings are given as a list which has a length being equal
    to the length of the number of constructors.
 
@@ -40,24 +26,37 @@
 *)
 
 ML {*
+  open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
+  fun mk_atom ty = Const (@{const_name atom}, ty --> @{typ atom});
+  val noatoms = @{term "{} :: atom set"};
+  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
+      if b = noatoms then a else
+      HOLogic.mk_binop @{const_name union} (a, b)) (rev sets) noatoms;
+  fun mk_diff a b =
+    if b = noatoms then a else
+    if b = a then noatoms else
+    HOLogic.mk_binop @{const_name minus} (a, b);
+*}
+
+atom_decl name
+
+datatype rlam =
+  rVar "name"
+| rApp "rlam" "rlam"
+| rLam "name" "rlam"
+
+ML {*
   val {descr, ...} = Datatype.the_info @{theory} "Fv.rlam";
   val sorts = [];
-  val noatoms = @{term "{} :: atom set"}
-  val binds = [[[]], [[], []], [[], [(NONE, 0)]]];
+  val binds = [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]]];
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
   val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
     "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
-      if b = noatoms then a else
-      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 minus} (a, b);
   fun fv_eq_constr i (cname, dts) bindcs =
     let
       val Ts = map (typ_of_dtyp descr sorts) dts;
@@ -71,15 +70,13 @@
       fun fv_arg ((dt, x), bindxs) =
         let
           val arg =
-            if is_rec_type dt then nth fv_frees (body_index dt) $ x
+            if is_rec_type dt then nth fv_frees (body_index dt) $ x else
             (* TODO: we just assume everything can be 'atomized' *)
-            else HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x]
+            HOLogic.mk_set @{typ atom} [mk_atom (type_of x) $ x]
           val sub = mk_union (map fv_bind bindxs)
         in
           mk_diff arg sub
         end;
-      val _ = tracing (string_of_int (length dts));
-      val _ = tracing (string_of_int (length bindcs));
     in
       (Attrib.empty_binding, HOLogic.mk_Trueprop (HOLogic.mk_eq
         (fv_c $ list_comb (c, args), mk_union (map fv_arg (dts ~~ args ~~ bindcs)))))