# HG changeset patch
# User blanchet
# Date 1514907654 -3600
# Node ID 6afba546f0e5efe34711c3fe9be309a9a3fd0425
# Parent  07176d5b81d51df16e7aba0952c01307f6f74302
updated dependencies + compile

diff -r 07176d5b81d5 -r 6afba546f0e5 src/HOL/Datatype_Examples/Compat.thy
--- 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>
diff -r 07176d5b81d5 -r 6afba546f0e5 src/HOL/Proofs/Extraction/Euclid.thy
--- 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>
diff -r 07176d5b81d5 -r 6afba546f0e5 src/HOL/Proofs/Extraction/Higman_Extraction.thy
--- 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]
diff -r 07176d5b81d5 -r 6afba546f0e5 src/HOL/Proofs/Extraction/Pigeonhole.thy
--- 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>
diff -r 07176d5b81d5 -r 6afba546f0e5 src/HOL/Proofs/Extraction/QuotRem.thy
--- 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>
diff -r 07176d5b81d5 -r 6afba546f0e5 src/HOL/Proofs/Extraction/Warshall.thy
--- 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>
diff -r 07176d5b81d5 -r 6afba546f0e5 src/HOL/Proofs/Lambda/WeakNorm.thy
--- 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>
diff -r 07176d5b81d5 -r 6afba546f0e5 src/HOL/Tools/Old_Datatype/old_datatype.ML
--- 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 =