diff -r 29c4a0cf9237 -r 6f01720fe520 Quot/Nominal/Fv.thy
--- a/Quot/Nominal/Fv.thy	Wed Feb 17 15:20:22 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Wed Feb 17 15:28:50 2010 +0100
@@ -67,7 +67,7 @@
   val {descr, ...} = Datatype.the_info @{theory} "Fv.rtrm1";
   val sorts = [];
   val bindsall = [
-    [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[], [], [(SOME @{term bv1}, 0)]]],
+    [[[]], [[], []], [[(NONE, 0)], [(NONE, 0)]], [[(NONE, 0)], [], [(SOME @{term bv1}, 0)]]],
     [[], [[]], [[], []]]
   ];
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
@@ -82,8 +82,10 @@
       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"});
-      (* TODO we assume that all can be 'atomized' *)
-      fun fv_bind (NONE, i) = mk_single_atom (nth args i)
+      fun fv_bind (NONE, i) =
+            if is_rec_type (nth dts i) then (nth fv_frees (body_index (nth dts i))) $ (nth args i) else
+            (* TODO we assume that all can be 'atomized' *)
+            mk_single_atom (nth args i)
         | fv_bind (SOME f, i) = f $ (nth args i);
       fun fv_arg ((dt, x), bindxs) =
         let