diff -r a40dbea68d0b -r 006d81399f6a Nominal/Fv.thy
--- a/Nominal/Fv.thy	Wed Mar 24 08:45:54 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 24 09:59:47 2010 +0100
@@ -278,8 +278,6 @@
 end
 *}
 
-ML AList.lookup
-
 (* We assume no bindings in the type on which bn is defined *)
 (* TODO: currently works only with current fv_bn function *)
 ML {*
@@ -296,8 +294,8 @@
     fun fv_arg ((dt, x), arg_no) =
       let
         val ty = fastype_of x
-        val _ = tracing (PolyML.makestring args_in_bn);
-        val _ = tracing (PolyML.makestring bn_fvbn);
+(*        val _ = tracing ("B 1" ^ PolyML.makestring args_in_bn);*)
+(*        val _ = tracing ("B 2" ^ PolyML.makestring bn_fvbn);*)
       in
         case AList.lookup (op=) args_in_bn arg_no of
           SOME NONE => @{term "{} :: atom set"}
@@ -420,7 +418,11 @@
     "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);
-  val nr_bns = non_rec_binds bindsall;
+(* TODO: We need a transitive closure, but instead we do this hack considering
+   all binding functions as recursive or not *)
+  val nr_bns =
+    if (non_rec_binds bindsall) = [] then []
+    else map (fn (bn, _, _) => bn) bns;
   val rel_bns = filter (fn (bn, _, _) => bn mem nr_bns) bns;
   val (bn_fv_bns, fv_bn_names_eqs) = fv_bns thy dt_info fv_frees rel_bns;
   val fvbns = map snd bn_fv_bns;