# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID d786fd77cf33c16a64edf359c03bdc5c43f3f83d
# Parent  e89c7ac4ce16d7dfd9529314fa40aae4d5a0019c
removed 'datatype_compat's that are no longer needed

diff -r e89c7ac4ce16 -r d786fd77cf33 src/HOL/Proofs/Extraction/Higman.thy
--- a/src/HOL/Proofs/Extraction/Higman.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Proofs/Extraction/Higman.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -16,8 +16,6 @@
 
 datatype_new letter = A | B
 
-datatype_compat letter
-
 inductive emb :: "letter list \<Rightarrow> letter list \<Rightarrow> bool"
 where
    emb0 [Pure.intro]: "emb [] bs"
diff -r e89c7ac4ce16 -r d786fd77cf33 src/HOL/Proofs/Extraction/Warshall.thy
--- a/src/HOL/Proofs/Extraction/Warshall.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Proofs/Extraction/Warshall.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -15,8 +15,6 @@
 
 datatype_new b = T | F
 
-datatype_compat b
-
 primrec
   is_path' :: "('a \<Rightarrow> 'a \<Rightarrow> b) \<Rightarrow> 'a \<Rightarrow> 'a list \<Rightarrow> 'a \<Rightarrow> bool"
 where
diff -r e89c7ac4ce16 -r d786fd77cf33 src/HOL/Proofs/Lambda/LambdaType.thy
--- a/src/HOL/Proofs/Lambda/LambdaType.thy	Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Proofs/Lambda/LambdaType.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -39,8 +39,6 @@
     Atom nat
   | Fun type type    (infixr "\<Rightarrow>" 200)
 
-datatype_compat type
-
 inductive typing :: "(nat \<Rightarrow> type) \<Rightarrow> dB \<Rightarrow> type \<Rightarrow> bool"  ("_ \<turnstile> _ : _" [50, 50, 50] 50)
   where
     Var [intro!]: "env x = T \<Longrightarrow> env \<turnstile> Var x : T"