src/HOL/Library/RBT_Impl.thy
changeset 49810 53f14f62cca2
parent 49807 9a0843995fd3
child 53374 a14d2a854c02
     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 *)