# HG changeset patch
# User haftmann
# Date 1285744081 -7200
# Node ID 863362a2d865cbc0520a0751b35741473ac0d20d
# Parent  9b1814140bcf95283a518f701744ff0a0f9f3df5
fact listsum now names listsum_foldl

diff -r 9b1814140bcf -r 863362a2d865 src/HOL/Nominal/Examples/Standardization.thy
--- 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