--- a/src/HOL/Datatype_Examples/Compat.thy Tue Jan 02 16:17:13 2018 +0100
+++ b/src/HOL/Datatype_Examples/Compat.thy Tue Jan 02 16:40:54 2018 +0100
@@ -8,7 +8,7 @@
section \<open>Tests for Compatibility with the Old Datatype Package\<close>
theory Compat
-imports "HOL-Library.Old_Datatype"
+imports Main
begin
subsection \<open>Viewing and Registering New-Style Datatypes as Old-Style Ones\<close>
--- a/src/HOL/Proofs/Extraction/Euclid.thy Tue Jan 02 16:17:13 2018 +0100
+++ b/src/HOL/Proofs/Extraction/Euclid.thy Tue Jan 02 16:40:54 2018 +0100
@@ -10,8 +10,8 @@
imports
"HOL-Computational_Algebra.Primes"
Util
- "HOL-Library.Old_Datatype"
"HOL-Library.Code_Target_Numeral"
+ "HOL-Library.Realizers"
begin
text \<open>
--- a/src/HOL/Proofs/Extraction/Higman_Extraction.thy Tue Jan 02 16:17:13 2018 +0100
+++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy Tue Jan 02 16:40:54 2018 +0100
@@ -6,7 +6,7 @@
subsection \<open>Extracting the program\<close>
theory Higman_Extraction
-imports Higman "HOL-Library.Old_Datatype" "HOL-Library.Open_State_Syntax"
+imports Higman "HOL-Library.Realizers" "HOL-Library.Open_State_Syntax"
begin
declare R.induct [ind_realizer]
--- a/src/HOL/Proofs/Extraction/Pigeonhole.thy Tue Jan 02 16:17:13 2018 +0100
+++ b/src/HOL/Proofs/Extraction/Pigeonhole.thy Tue Jan 02 16:40:54 2018 +0100
@@ -5,7 +5,7 @@
section \<open>The pigeonhole principle\<close>
theory Pigeonhole
-imports Util "HOL-Library.Old_Datatype" "HOL-Library.Code_Target_Numeral"
+imports Util "HOL-Library.Realizers" "HOL-Library.Code_Target_Numeral"
begin
text \<open>
--- a/src/HOL/Proofs/Extraction/QuotRem.thy Tue Jan 02 16:17:13 2018 +0100
+++ b/src/HOL/Proofs/Extraction/QuotRem.thy Tue Jan 02 16:40:54 2018 +0100
@@ -5,7 +5,7 @@
section \<open>Quotient and remainder\<close>
theory QuotRem
-imports "HOL-Library.Old_Datatype" Util
+imports Util "HOL-Library.Realizers"
begin
text \<open>Derivation of quotient and remainder using program extraction.\<close>
--- a/src/HOL/Proofs/Extraction/Warshall.thy Tue Jan 02 16:17:13 2018 +0100
+++ b/src/HOL/Proofs/Extraction/Warshall.thy Tue Jan 02 16:40:54 2018 +0100
@@ -5,7 +5,7 @@
section \<open>Warshall's algorithm\<close>
theory Warshall
-imports "HOL-Library.Old_Datatype"
+imports "HOL-Library.Realizers"
begin
text \<open>
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy Tue Jan 02 16:17:13 2018 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Tue Jan 02 16:40:54 2018 +0100
@@ -6,7 +6,7 @@
section \<open>Weak normalization for simply-typed lambda calculus\<close>
theory WeakNorm
-imports LambdaType NormalForm "HOL-Library.Old_Datatype" "HOL-Library.Code_Target_Int"
+imports LambdaType NormalForm "HOL-Library.Realizers" "HOL-Library.Code_Target_Int"
begin
text \<open>
--- a/src/HOL/Tools/Old_Datatype/old_datatype.ML Tue Jan 02 16:17:13 2018 +0100
+++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML Tue Jan 02 16:40:54 2018 +0100
@@ -18,7 +18,6 @@
val check_specs: spec list -> theory -> spec list * Proof.context
val add_datatype: config -> spec list -> theory -> string list * theory
val add_datatype_cmd: config -> spec_cmd list -> theory -> string list * theory
- val spec_cmd: spec_cmd parser
end;
structure Old_Datatype : OLD_DATATYPE =