# HG changeset patch
# User blanchet
# Date 1410288696 -7200
# Node ID 9f0bfcd150971b3a9c6703c4a7dbf678bc8308a1
# Parent  61d94335ef6c6739206fbb8ff9ff5a202e6d5ae7
ported HOL-Proofs-Lambda to new datatypes

diff -r 61d94335ef6c -r 9f0bfcd15097 src/HOL/Proofs/Lambda/Eta.thy
--- 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)
diff -r 61d94335ef6c -r 9f0bfcd15097 src/HOL/Proofs/Lambda/Lambda.thy
--- 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
diff -r 61d94335ef6c -r 9f0bfcd15097 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
@@ -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)