--- a/Quot/Nominal/Test.thy	Wed Jan 27 18:06:14 2010 +0100
+++ b/Quot/Nominal/Test.thy	Wed Jan 27 18:26:01 2010 +0100
@@ -117,11 +117,11 @@
     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
-    @{term "{}"}
+    HOLogic.mk_set @{typ name} []
   val fv_eq = 
-    if null vars then HOLogic.mk_set @{typ atom} []
+    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 fv_eq
+  val fv_eq_str = Syntax.string_of_term lthy (Syntax.check_term lthy fv_eq)
 in
   prefix ^ " (" ^ (Binding.name_of name) ^ " " ^ (implode (separate " " var_strs)) ^ ") = " ^ fv_eq_str
 end