diff -r bfa48c000aa7 -r 478c5648e73f Nominal/Ex/Ex1.thy --- a/Nominal/Ex/Ex1.thy Wed Dec 22 23:12:51 2010 +0000 +++ b/Nominal/Ex/Ex1.thy Thu Dec 23 00:22:41 2010 +0000 @@ -40,8 +40,8 @@ thm foo_bar.supp lemma - "fv_foo (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}" -apply(simp only: foo_bar.fv_defs) + "supp (Foo1 (Bar1 v x (Bar0 x)) (Foo0 v)) = {}" +apply(simp only: foo_bar.supp) apply(simp only: foo_bar.bn_defs) apply(simp only: supp_at_base) apply(simp)