diff -r dce45db16063 -r c1af17982f98 Quot/Nominal/Test.thy
--- a/Quot/Nominal/Test.thy	Wed Feb 03 10:50:24 2010 +0100
+++ b/Quot/Nominal/Test.thy	Wed Feb 03 11:21:34 2010 +0100
@@ -131,7 +131,7 @@
   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
-      fv_bds s bds (Free ("fv_" ^ (Long_Name.base_name tyS), Type ("fun", [dummyT, @{typ "name set"}])) $ t) else
+      fv_bds s bds (Free ("rfv_" ^ (Long_Name.base_name tyS), Type ("fun", [dummyT, @{typ "name set"}])) $ t) else
     HOLogic.mk_set @{typ name} []
   val fv_eq =
     if null vars then HOLogic.mk_set @{typ name} []
@@ -155,7 +155,7 @@
 
 ML {*
 fun fv_dt lthy dt_names (((s2, s3), syn), constrs) =
-    map (fv_constr lthy ("fv_" ^ Binding.name_of s3) dt_names) constrs
+    map (fv_constr lthy ("rfv_" ^ Binding.name_of s3) dt_names) constrs
  |> separate "\n"
  |> implode
 *}