From feb385748f99ede80afdcebb89cfd3adf94e96cf Mon Sep 17 00:00:00 2001
From: Jeremy Avigad <avigad@cmu.edu>
Date: Sun, 7 Jun 2015 11:43:23 +1000
Subject: [PATCH] refactor(library/data/set/map.lean): put map into set
 namespace

This is needed to repair a conflict in the tutorial, but it is the right thing to do anyhow. The type "map A B" should not be a top-level identifier.
---
 library/data/set/map.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/library/data/set/map.lean b/library/data/set/map.lean
index f710a68ac..e39bccdcd 100644
--- a/library/data/set/map.lean
+++ b/library/data/set/map.lean
@@ -6,7 +6,9 @@ Author: Jeremy Avigad, Andrew Zipperer
 Functions between subsets of finite types, bundled with the domain and range.
 -/
 import data.set.function
-open eq.ops set
+open eq.ops
+
+namespace set
 
 record map {X Y : Type} (a : set X) (b : set Y) := (func : X → Y) (mapsto : maps_to func a b)
 attribute map.func [coercion]
@@ -164,3 +166,4 @@ and.intro
   (surjective_of_right_inverse (and.right H))
 
 end map
+end set