# HG changeset patch
# User blanchet
# Date 1409695586 -7200
# Node ID 47c3c7019b976dd122f5b0e846950803f85ced3b
# Parent  ca7ea280e906d42cfd49cc75b24708c2e0971610
tuned imports

diff -r ca7ea280e906 -r 47c3c7019b97 src/HOL/Main.thy
--- a/src/HOL/Main.thy	Wed Sep 03 00:06:25 2014 +0200
+++ b/src/HOL/Main.thy	Wed Sep 03 00:06:26 2014 +0200
@@ -2,7 +2,7 @@
 
 theory Main
 imports Predicate_Compile Quickcheck_Narrowing Extraction Lifting_Sum Coinduction Nitpick
-  BNF_Greatest_Fixpoint
+  BNF_Greatest_Fixpoint Old_Datatype
 begin
 
 text {*
diff -r ca7ea280e906 -r 47c3c7019b97 src/HOL/Num.thy
--- a/src/HOL/Num.thy	Wed Sep 03 00:06:25 2014 +0200
+++ b/src/HOL/Num.thy	Wed Sep 03 00:06:26 2014 +0200
@@ -6,7 +6,7 @@
 header {* Binary Numerals *}
 
 theory Num
-imports BNF_Least_Fixpoint Old_Datatype
+imports BNF_Least_Fixpoint
 begin
 
 subsection {* The @{text num} type *}
diff -r ca7ea280e906 -r 47c3c7019b97 src/HOL/Option.thy
--- a/src/HOL/Option.thy	Wed Sep 03 00:06:25 2014 +0200
+++ b/src/HOL/Option.thy	Wed Sep 03 00:06:26 2014 +0200
@@ -5,7 +5,7 @@
 header {* Datatype option *}
 
 theory Option
-imports BNF_Least_Fixpoint Old_Datatype Finite_Set
+imports BNF_Least_Fixpoint Finite_Set
 begin
 
 datatype_new 'a option =