src/HOL/Library/RBT_Impl.thy
changeset 37591 d3daea901123
parent 37458 4a76497f2eaa
child 39198 f967a16dfcdd
     1.1 --- a/src/HOL/Library/RBT_Impl.thy	Mon Jun 28 15:03:07 2010 +0200
     1.2 +++ b/src/HOL/Library/RBT_Impl.thy	Mon Jun 28 15:03:07 2010 +0200
     1.3 @@ -1076,7 +1076,7 @@
     1.4    from this Empty_is_rbt have
     1.5      "lookup (More_List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
     1.6       by (simp add: `ys = rev xs`)
     1.7 -  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev prod_case_split)
     1.8 +  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev)
     1.9  qed
    1.10  
    1.11  hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted