--- a/src/HOL/Proofs/Lambda/Eta.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Proofs/Lambda/Eta.thy Tue Sep 09 20:51:36 2014 +0200
@@ -181,9 +181,9 @@
apply simp
apply (rule iffI)
apply (erule linorder_neqE)
- apply (rule_tac x = "Var nat" in exI)
+ apply (rename_tac nat a, rule_tac x = "Var nat" in exI)
apply simp
- apply (rule_tac x = "Var (nat - 1)" in exI)
+ apply (rename_tac nat a, rule_tac x = "Var (nat - 1)" in exI)
apply simp
apply clarify
apply (rule notE)
--- a/src/HOL/Proofs/Lambda/Lambda.thy Tue Sep 09 20:51:36 2014 +0200
+++ b/src/HOL/Proofs/Lambda/Lambda.thy Tue Sep 09 20:51:36 2014 +0200
@@ -12,7 +12,7 @@
subsection {* Lambda-terms in de Bruijn notation and substitution *}
-datatype dB =
+datatype_new dB =
Var nat
| App dB dB (infixl "\<degree>" 200)
| Abs dB
--- 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
@@ -35,10 +35,12 @@
subsection {* Types and typing rules *}
-datatype type =
+datatype_new type =
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"
@@ -225,9 +227,11 @@
apply simp
apply (erule list_app_typeE)
apply (ind_cases "e \<turnstile> t \<degree> u : T" for t u T)
+ apply (rename_tac nat Tsa Ta)
apply (drule_tac T="Atom nat" and U="Ta \<Rightarrow> Tsa \<Rrightarrow> T" in var_app_type_eq)
apply assumption
apply simp
+ apply (rename_tac nat type1 type2)
apply (erule_tac x="ts @ [a]" in allE)
apply (erule_tac x="Ts @ [type1]" in allE)
apply (erule_tac x="type2" in allE)
@@ -270,6 +274,7 @@
apply (erule typing.cases)
apply simp_all
apply atomize
+ apply (rename_tac type1 type2)
apply (erule_tac x="type1" in allE)
apply (erule_tac x="type2" in allE)
apply (erule mp)