fix code equation for RBT_Impl.fold
authorAndreas Lochbihler
Wed Oct 10 16:18:27 2012 +0200 (2012-10-10)
changeset 4981053f14f62cca2
parent 49809 39db47ed6d54
child 49811 3fc6b3289c31
fix code equation for RBT_Impl.fold
src/HOL/Library/RBT_Impl.thy
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Wed Oct 10 15:17:18 2012 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Wed Oct 10 16:18:27 2012 +0200
     1.3 @@ -1076,8 +1076,8 @@
     1.4    by (simp_all add: fold_def fun_eq_iff)
     1.5  
     1.6  lemma fold_code [code]:
     1.7 -  "fold f Empty c = c"
     1.8 -  "fold f (Branch c lt k v rt) c = fold f rt (f k v (fold f lt c))"
     1.9 +  "fold f Empty x = x"
    1.10 +  "fold f (Branch c lt k v rt) x = fold f rt (f k v (fold f lt x))"
    1.11  by(simp_all)
    1.12  
    1.13  (* fold with continuation predicate *)