# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1265192494 -3600
# Node ID c1af17982f986f40894da55ee01dd3ef81daa87e
# Parent  dce45db1606340f9cce269ededd4b4a5c2d1771e
Minor

diff -r dce45db16063 -r c1af17982f98 Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Wed Feb 03 10:50:24 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Wed Feb 03 11:21:34 2010 +0100
@@ -138,7 +138,7 @@
   apply(rule_tac x="pi \<bullet> pia" in exI)
   apply(simp add: alpha_gen.simps)
   apply(erule conjE)+
-  apply(rule conjI)+
+  apply(rule conjI)
   apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
   apply(simp add: a[symmetric] atom_eqvt eqvts)
   apply(rule conjI)
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
 *}