diff -r 758904445fb2 -r d1293d30c657 Nominal/ExLet.thy
--- a/Nominal/ExLet.thy	Fri Mar 26 17:22:02 2010 +0100
+++ b/Nominal/ExLet.thy	Fri Mar 26 17:22:17 2010 +0100
@@ -87,7 +87,7 @@
   apply (simp add: permute_bn_alpha_bn)
   apply (simp add: perm_bn[symmetric])
   apply (simp add: eqvts[symmetric])
-  apply (simp add: supp_Abs)
+  apply (simp add: supp_abs)
   apply (simp add: trm_lts.supp)
   apply (rule supp_perm_eq[symmetric])
   apply (subst supp_finite_atom_set)
@@ -157,10 +157,10 @@
     apply(rule at_set_avoiding2)
     apply(rule fin_bn)
     apply(simp add: finite_supp)
-    apply(simp add: supp_Abs)
+    apply(simp add: supp_abs)
     apply(rule finite_Diff)
     apply(simp add: finite_supp)
-    apply(simp add: fresh_star_def fresh_def supp_Abs)
+    apply(simp add: fresh_star_def fresh_def supp_abs)
     apply(simp add: eqvts permute_bn)
     apply(rule a5)
     apply(simp add: permute_bn)