--- 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]]
--- 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]]
--- 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 {*