Nominal/Ex/Ex1.thy
changeset 2625 478c5648e73f
parent 2611 3d101f2f817c
child 2950 0911cb7bf696
--- 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)