--- a/src/HOL/Nominal/Examples/Standardization.thy Wed Sep 29 09:08:00 2010 +0200
+++ b/src/HOL/Nominal/Examples/Standardization.thy Wed Sep 29 09:08:01 2010 +0200
@@ -213,7 +213,7 @@
prefer 2
apply (erule allE, erule impE, rule refl, erule spec)
apply simp
- apply (metis add_strict_increasing le_add1 length_pos_if_in_set listsum listsum_map_remove1 nat_add_commute)
+ apply (metis add_strict_increasing le_add1 length_pos_if_in_set listsum_foldl listsum_map_remove1 nat_add_commute)
apply clarify
apply (subgoal_tac "\<exists>y::name. y \<sharp> (x, u, z)")
prefer 2