# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1264613161 -3600
# Node ID b582f7decd9a14eff6e5d9ae9203b40e99c5b3b6
# Parent  9913c5695fc751a160d1ce1c2d01f63495d72178
Correct types which fixes the printing.

diff -r 9913c5695fc7 -r b582f7decd9a Quot/Nominal/Test.thy
--- 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