From 854e72e6653edf63ba69afc9f534a011810dd64a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 Oct 2014 15:32:42 -0700
Subject: [PATCH] refactor(library/data/list): minimize dependencies and avoid
 'sorry' warning

---
 library/data/list/basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 1075d8094..bf762858f 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -3,7 +3,7 @@
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
-import logic tools.helper_tactics tools.tactic data.nat
+import logic tools.helper_tactics tools.tactic data.nat.basic
 
 -- Theory list
 -- ===========