src/HOL/Library/RBT_Impl.thy
changeset 46133 d9fe85d3d2cd
parent 45990 b7b905b23b2a
child 47397 d654c73e4b12
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Fri Jan 06 10:19:49 2012 +0100
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Fri Jan 06 10:19:49 2012 +0100
     1.3 @@ -1049,7 +1049,7 @@
     1.4  subsection {* Folding over entries *}
     1.5  
     1.6  definition fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<Rightarrow> 'c) \<Rightarrow> ('a, 'b) rbt \<Rightarrow> 'c \<Rightarrow> 'c" where
     1.7 -  "fold f t = More_List.fold (prod_case f) (entries t)"
     1.8 +  "fold f t = List.fold (prod_case f) (entries t)"
     1.9  
    1.10  lemma fold_simps [simp, code]:
    1.11    "fold f Empty = id"
    1.12 @@ -1071,12 +1071,12 @@
    1.13  proof -
    1.14    obtain ys where "ys = rev xs" by simp
    1.15    have "\<And>t. is_rbt t \<Longrightarrow>
    1.16 -    lookup (More_List.fold (prod_case insert) ys t) = lookup t ++ map_of (rev ys)"
    1.17 +    lookup (List.fold (prod_case insert) ys t) = lookup t ++ map_of (rev ys)"
    1.18        by (induct ys) (simp_all add: bulkload_def lookup_insert prod_case_beta)
    1.19    from this Empty_is_rbt have
    1.20 -    "lookup (More_List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
    1.21 +    "lookup (List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
    1.22       by (simp add: `ys = rev xs`)
    1.23 -  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev)
    1.24 +  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_def)
    1.25  qed
    1.26  
    1.27  hide_const (open) R B Empty insert delete entries keys bulkload lookup map_entry map fold union sorted