diff -r dd874e6a3282 -r f274975039b2 src/HOL/Nominal/Examples/SOS.thy
--- a/src/HOL/Nominal/Examples/SOS.thy	Thu Jun 21 13:23:33 2007 +0200
+++ b/src/HOL/Nominal/Examples/SOS.thy	Thu Jun 21 13:49:27 2007 +0200
@@ -286,19 +286,21 @@
 declare ty.inject  [simp add]
 declare data.inject [simp add]
 
-inductive_cases2 t_Lam_inv_auto[elim]: "\<Gamma> \<turnstile> Lam [x].t : T"
-inductive_cases2 t_Var_inv_auto[elim]: "\<Gamma> \<turnstile> Var x : T"
-inductive_cases2 t_App_inv_auto[elim]: "\<Gamma> \<turnstile> App x y : T"
-inductive_cases2 t_Const_inv_auto[elim]: "\<Gamma> \<turnstile> Const n : T"
-inductive_cases2 t_Fst_inv_auto[elim]: "\<Gamma> \<turnstile> Fst x : T"
-inductive_cases2 t_Snd_inv_auto[elim]: "\<Gamma> \<turnstile> Snd x : T"
-inductive_cases2 t_InL_inv_auto[elim]: "\<Gamma> \<turnstile> InL x : T"
-inductive_cases2 t_InL_inv_auto'[elim]: "\<Gamma> \<turnstile> InL x : Data (DSum T\<^isub>1 T2)"
-inductive_cases2 t_InR_inv_auto[elim]: "\<Gamma> \<turnstile> InR x : T"
-inductive_cases2 t_InR_inv_auto'[elim]: "\<Gamma> \<turnstile> InR x : Data (DSum T\<^isub>1 T2)"
-inductive_cases2 t_Pr_inv_auto[elim]:  "\<Gamma> \<turnstile> Pr x y : T"
-inductive_cases2 t_Pr_inv_auto'[elim]: "\<Gamma> \<turnstile> Pr e\<^isub>1 e\<^isub>2 : Data (DProd \<sigma>1 \<sigma>\<^isub>2)"
-inductive_cases2 t_Case_inv_auto[elim]: "\<Gamma> \<turnstile> Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 : T"
+
+inductive_cases2 typing_inv_auto[elim]: 
+  "\<Gamma> \<turnstile> Lam [x].t : T"
+  "\<Gamma> \<turnstile> Var x : T"
+  "\<Gamma> \<turnstile> App x y : T"
+  "\<Gamma> \<turnstile> Const n : T"
+  "\<Gamma> \<turnstile> Fst x : T"
+  "\<Gamma> \<turnstile> Snd x : T"
+  "\<Gamma> \<turnstile> InL x : T"
+  "\<Gamma> \<turnstile> InL x : Data (DSum T\<^isub>1 T2)"
+  "\<Gamma> \<turnstile> InR x : T"
+  "\<Gamma> \<turnstile> InR x : Data (DSum T\<^isub>1 T2)"
+  "\<Gamma> \<turnstile> Pr x y : T"
+  "\<Gamma> \<turnstile> Pr e\<^isub>1 e\<^isub>2 : Data (DProd \<sigma>1 \<sigma>\<^isub>2)"
+  "\<Gamma> \<turnstile> Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 : T"
 
 declare trm.inject [simp del]
 declare ty.inject [simp del]
@@ -528,15 +530,16 @@
 declare ty.inject  [simp add]
 declare data.inject [simp add]
 
-inductive_cases2 b_App_inv_auto[elim]: "App e\<^isub>1 e\<^isub>2 \<Down> t" 
-inductive_cases2 b_Case_inv_auto[elim]: "Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 \<Down> t"
-inductive_cases2 b_Lam_inv_auto[elim]: "Lam[x].t \<Down> t"
-inductive_cases2 b_Const_inv_auto[elim]: "Const n \<Down> t"
-inductive_cases2 b_Fst_inv_auto[elim]: "Fst e \<Down> t"
-inductive_cases2 b_Snd_inv_auto[elim]: "Snd e \<Down> t"
-inductive_cases2 b_InL_inv_auto[elim]: "InL e \<Down> t"
-inductive_cases2 b_InR_inv_auto[elim]: "InR e \<Down> t"
-inductive_cases2 b_Pr_inv_auto[elim]: "Pr e\<^isub>1 e\<^isub>2 \<Down> t"
+inductive_cases2 b_inv_auto[elim]: 
+  "App e\<^isub>1 e\<^isub>2 \<Down> t" 
+  "Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2 \<Down> t"
+  "Lam[x].t \<Down> t"
+  "Const n \<Down> t"
+  "Fst e \<Down> t"
+  "Snd e \<Down> t"
+  "InL e \<Down> t"
+  "InR e \<Down> t"
+  "Pr e\<^isub>1 e\<^isub>2 \<Down> t"
 
 declare trm.inject  [simp del]
 declare ty.inject  [simp del]
@@ -547,7 +550,7 @@
   obtains f\<^isub>1 and f\<^isub>2 where "e\<^isub>1 \<Down> Lam [x]. f\<^isub>1" "e\<^isub>2 \<Down> f\<^isub>2" "f\<^isub>1[x::=f\<^isub>2] \<Down> e'"
   using assms
   apply -
-  apply(erule b_App_inv_auto)
+  apply(erule b_inv_auto)
   apply(drule_tac pi="[(xa,x)]" in big.eqvt)
   apply(drule_tac pi="[(xa,x)]" in big.eqvt)
   apply(drule_tac pi="[(xa,x)]" in big.eqvt)
@@ -561,7 +564,7 @@
   obtains e' where "e \<Down> InL e'" and "e\<^isub>1[x\<^isub>1::=e'] \<Down> e''"
   using assms 
   apply -
-  apply(rule b_Case_inv_auto)
+  apply(rule b_inv_auto(2))
   apply(auto)
   apply(simp add: alpha)
   apply(auto)
@@ -590,7 +593,7 @@
   obtains e' where "e \<Down> InR e'" and "e\<^isub>2[x\<^isub>2::=e'] \<Down> e''"
   using assms 
   apply -
-  apply(rule b_Case_inv_auto)
+  apply(rule b_inv_auto(2))
   apply(auto)
   apply(simp add: alpha)
   apply(auto)
@@ -625,16 +628,17 @@
 declare ty.inject  [simp add]
 declare data.inject [simp add]
 
-inductive_cases2 v_Const_inv_auto[elim]: "val (Const n)"
-inductive_cases2 v_Pr_inv_auto[elim]: "val (Pr e\<^isub>1 e\<^isub>2)"
-inductive_cases2 v_InL_inv_auto[elim]: "val (InL e)"
-inductive_cases2 v_InR_inv_auto[elim]: "val (InR e)"
-inductive_cases2 v_Fst_inv_auto[elim]: "val (Fst e)"
-inductive_cases2 v_Snd_inv_auto[elim]: "val (Snd e)"
-inductive_cases2 v_Case_inv_auto[elim]: "val (Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2)"
-inductive_cases2 v_Var_inv_auto[elim]: "val (Var x)"
-inductive_cases2 v_Lam_inv_auto[elim]: "val (Lam [x].e)"
-inductive_cases2 v_App_inv_auto[elim]: "val (App e\<^isub>1 e\<^isub>2)"
+inductive_cases2 v_inv_auto[elim]: 
+  "val (Const n)"
+  "val (Pr e\<^isub>1 e\<^isub>2)"
+  "val (InL e)"
+  "val (InR e)"
+  "val (Fst e)"
+  "val (Snd e)"
+  "val (Case e of inl x\<^isub>1 \<rightarrow> e\<^isub>1 | inr x\<^isub>2 \<rightarrow> e\<^isub>2)"
+  "val (Var x)"
+  "val (Lam [x].e)"
+  "val (App e\<^isub>1 e\<^isub>2)"
 
 declare trm.inject  [simp del]
 declare ty.inject  [simp del]