# HG changeset patch
# User haftmann
# Date 1216107039 -7200
# Node ID bc47d30747e615650271ead76543ca7caee9461a
# Parent  3ac9e3cd1fa39962f57e09a9f2785f3508f3a6e3
dropped map; fixed swap

diff -r 3ac9e3cd1fa3 -r bc47d30747e6 src/HOL/Library/Array.thy
--- a/src/HOL/Library/Array.thy	Tue Jul 15 07:10:50 2008 +0200
+++ b/src/HOL/Library/Array.thy	Tue Jul 15 09:30:39 2008 +0200
@@ -77,7 +77,7 @@
   "swap i x a = (do
      y \<leftarrow> nth a i;
      upd i x a;
-     return x
+     return y
    done)"
 
 definition
@@ -93,15 +93,7 @@
      mapM (nth a) [0..<n]
    done)"
 
-definition
-  map :: "('a\<Colon>heap \<Rightarrow> 'a) \<Rightarrow> 'a array \<Rightarrow> 'a array Heap"
-where
-  "map f a = (do
-     n \<leftarrow> length a;
-     foldM (\<lambda>n. map_entry n f) [0..<n] a
-   done)"
-
-hide (open) const new map -- {* avoid clashed with some popular names *}
+hide (open) const new -- {* avoid clashed with some popular names *}
 
 
 subsection {* Properties *}