changeset 3235 | 5ebd327ffb96 |
parent 3217 | d67a6a48f1c7 |
child 3236 | e2da10806a34 |
--- a/Nominal/Ex/Local_Contexts.thy Mon May 19 11:19:48 2014 +0100 +++ b/Nominal/Ex/Local_Contexts.thy Mon May 19 12:45:26 2014 +0100 @@ -29,7 +29,7 @@ lemma atom_image_set_eq_supp: "atom ` set xs = supp xs" by (metis image_set set_map_atom_eq_supp) -nominal_primrec (in name_subst) +nominal_function (in name_subst) subst :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> lam" ("_[_::=_]" [120,120,120] 120) where "(Var x)[xs::=t] = name_subst x xs t"