--- a/Quot/Nominal/Test.thy	Wed Jan 27 17:39:13 2010 +0100
+++ b/Quot/Nominal/Test.thy	Wed Jan 27 18:06:14 2010 +0100
@@ -99,16 +99,13 @@
    ^ (Pretty.str_of (Syntax.pretty_mixfix syn)))
 *}
 
-ML Local_Theory.exit_global
-
-(* TODO: replace with proper thing *)
+(* TODO: replace with the proper thing *)
 ML {*
-fun is_atom ty = ty = "name"
+fun is_atom ty = ty = "Test.name"
 *}
 
-ML {* @{term "A \<union> B"} *}
-
-(* TODO: After variant_frees, check that the new names correspond to the ones given by user *)
+(* 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 {*
 fun fv_constr lthy prefix dt_names (((name, anno_tys), bds), syn) =
 let
@@ -118,7 +115,8 @@
   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 tyS mem dt_names then Free ("fv_" ^ tyS, dummyT) $ 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
     @{term "{}"}
   val fv_eq = 
     if null vars then HOLogic.mk_set @{typ atom} []