# HG changeset patch # User Cezary Kaliszyk # 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 \ 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 *}