--- a/Quot/Nominal/Test.thy	Thu Jan 28 10:26:36 2010 +0100
+++ b/Quot/Nominal/Test.thy	Thu Jan 28 10:52:10 2010 +0100
@@ -104,6 +104,21 @@
 fun is_atom ty = ty = "Test.name"
 *}
 
+ML {*
+fun fv_bds s bds set =
+  case bds of
+    [] => set
+  | B (s1, s2) :: tl => 
+      if s2 = s then 
+        fv_bds s tl (HOLogic.mk_binop @{const_name "HOL.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})]))
+      else fv_bds s tl set
+  | BS (s1, s2) :: tl =>
+    (* TODO: This is just a copy *)
+      if s2 = s then 
+        fv_bds s tl (HOLogic.mk_binop @{const_name "HOL.minus_class.minus"} (set, HOLogic.mk_set @{typ name} [Free (s1, @{typ name})]))
+      else fv_bds s tl set
+*}
+
 (* TODO: After variant_frees, check that the new names correspond to the ones given by user
    so that 'bind' is matched with variables correctly *)
 ML {*
@@ -115,10 +130,10 @@
   val var_strs = map (Syntax.string_of_term lthy) vars;
   fun fv_var (t as Free (s, (ty as Type (tyS, _)))) =
     if is_atom tyS then HOLogic.mk_set ty [t] else
-    if (Long_Name.base_name tyS) mem dt_names then 
-      Free ("fv_" ^ (Long_Name.base_name tyS), Type ("fun", [dummyT, @{typ "name set"}])) $ t else
+    if (Long_Name.base_name tyS) mem dt_names then
+      fv_bds s bds (Free ("fv_" ^ (Long_Name.base_name tyS), Type ("fun", [dummyT, @{typ "name set"}])) $ t) else
     HOLogic.mk_set @{typ name} []
-  val fv_eq = 
+  val fv_eq =
     if null vars then HOLogic.mk_set @{typ name} []
     else foldr1 (HOLogic.mk_binop @{const_name union}) (map fv_var vars)
   val fv_eq_str = Syntax.string_of_term lthy (Syntax.check_term lthy fv_eq)