# HG changeset patch
# User wenzelm
# Date 1438722676 -7200
# Node ID 144523e0678e7eb836afc26212844b0880d49d1e
# Parent  9043fd2c8cb6bfbfe786d98624886e392c5b5a42
eliminated clone;

diff -r 9043fd2c8cb6 -r 144523e0678e NEWS
--- a/NEWS	Tue Aug 04 15:00:58 2015 +0200
+++ b/NEWS	Tue Aug 04 23:11:16 2015 +0200
@@ -172,6 +172,9 @@
 
 *** HOL ***
 
+* Theory Map: lemma map_of_is_SomeD was a clone of map_of_SomeD and has
+been removed. INCOMPATIBILITY.
+
 * Quickcheck setup for finite sets.
 
 * Discontinued simp_legacy_precond. Potential INCOMPATIBILITY.
diff -r 9043fd2c8cb6 -r 144523e0678e src/HOL/Map.thy
--- a/src/HOL/Map.thy	Tue Aug 04 15:00:58 2015 +0200
+++ b/src/HOL/Map.thy	Tue Aug 04 23:11:16 2015 +0200
@@ -137,12 +137,6 @@
   "(map_of xys x = None) = (x \<notin> fst ` (set xys))"
 by (induct xys) simp_all
 
-lemma map_of_is_SomeD: "map_of xys x = Some y \<Longrightarrow> (x,y) \<in> set xys"
-apply (induct xys)
- apply simp
-apply (clarsimp split: if_splits)
-done
-
 lemma map_of_eq_Some_iff [simp]:
   "distinct(map fst xys) \<Longrightarrow> (map_of xys x = Some y) = ((x,y) \<in> set xys)"
 apply (induct xys)
@@ -229,7 +223,7 @@
 done
 
 lemma map_of_SomeD: "map_of xs k = Some y \<Longrightarrow> (k, y) \<in> set xs"
-by (induct xs) (simp, atomize (full), auto)
+  by (induct xs) (auto split: if_splits)
 
 lemma map_of_mapk_SomeI:
   "inj f \<Longrightarrow> map_of t k = Some x \<Longrightarrow>