# HG changeset patch
# User blanchet
# Date 1411059710 -7200
# Node ID 2ee61d28c667de432c9aa0655112d96db9ca3f03
# Parent  0e8d82e95dd23e0e208e9e3020b9dcbac63ac2f9
tuned imports

diff -r 0e8d82e95dd2 -r 2ee61d28c667 src/HOL/Proofs/Lambda/Lambda.thy
--- a/src/HOL/Proofs/Lambda/Lambda.thy	Thu Sep 18 18:49:58 2014 +0200
+++ b/src/HOL/Proofs/Lambda/Lambda.thy	Thu Sep 18 19:01:50 2014 +0200
@@ -6,7 +6,7 @@
 header {* Basic definitions of Lambda-calculus *}
 
 theory Lambda
-imports Old_Datatype
+imports Main
 begin
 
 declare [[syntax_ambiguity_warning = false]]
diff -r 0e8d82e95dd2 -r 2ee61d28c667 src/HOL/Proofs/Lambda/ListOrder.thy
--- a/src/HOL/Proofs/Lambda/ListOrder.thy	Thu Sep 18 18:49:58 2014 +0200
+++ b/src/HOL/Proofs/Lambda/ListOrder.thy	Thu Sep 18 19:01:50 2014 +0200
@@ -6,7 +6,7 @@
 header {* Lifting an order to lists of elements *}
 
 theory ListOrder
-imports Old_Datatype
+imports Main
 begin
 
 declare [[syntax_ambiguity_warning = false]]
diff -r 0e8d82e95dd2 -r 2ee61d28c667 src/HOL/Proofs/Lambda/WeakNorm.thy
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy	Thu Sep 18 18:49:58 2014 +0200
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy	Thu Sep 18 19:01:50 2014 +0200
@@ -6,7 +6,8 @@
 header {* Weak normalization for simply-typed lambda calculus *}
 
 theory WeakNorm
-imports LambdaType NormalForm "~~/src/HOL/Library/Code_Target_Int"
+imports LambdaType NormalForm "~~/src/HOL/Library/Old_Datatype"
+  "~~/src/HOL/Library/Code_Target_Int"
 begin
 
 text {*