# HG changeset patch
# User haftmann
# Date 1447487151 -3600
# Node ID 9a51e4dfc5d999fa26230f1dc8a7c5f6507bd420
# Parent  4b53042d7a40b02d36261d496ff3122419fd9fc5
reverted half-baken 7d1127ac2251

diff -r 4b53042d7a40 -r 9a51e4dfc5d9 src/HOL/List.thy
--- a/src/HOL/List.thy	Sat Nov 14 08:45:51 2015 +0100
+++ b/src/HOL/List.thy	Sat Nov 14 08:45:51 2015 +0100
@@ -6408,15 +6408,6 @@
   "map f (filter P xs) = map_filter (\<lambda>x. if P x then Some (f x) else None) xs"
   by (simp add: map_filter_def)
 
-definition map_range :: "(nat \<Rightarrow> 'a) \<Rightarrow> nat \<Rightarrow> 'a list"
-where
-  [code_abbrev]: "map_range f n = map f [0..<n]"
-
-lemma map_range_simps [simp, code]:
-  "map_range f 0 = []"
-  "map_range f (Suc n) = map_range f n @ [f n]"
-  by (simp_all add: map_range_def)
-
 text \<open>Optimized code for @{text"\<forall>i\<in>{a..b::int}"} and @{text"\<forall>n:{a..<b::nat}"}
 and similiarly for @{text"\<exists>"}.\<close>