--- 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"
--- 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
--- 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"