--- a/Nominal/Test_compat1.thy	Tue Mar 09 11:06:57 2010 +0100
+++ b/Nominal/Test_compat1.thy	Tue Mar 09 11:36:40 2010 +0100
@@ -103,8 +103,28 @@
    \<Longrightarrow> Alpha_lam (LET bp lam) (LET bp' lam')"
 | "Alpha_lam lam lam' \<and> name = name' \<Longrightarrow> Alpha_bp (BP name lam) (BP name' lam')"
 | "Alpha_lam (pi \<bullet> t) t' \<Longrightarrow> Compat_bp (BP x t) pi (BP x' t')"
-
-
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding Alpha_inj}, []), (build_alpha_inj @{thms Alpha_lam_Alpha_bp_Compat_bp.intros} @{thms lam_raw.distinct lam_raw.inject bp_raw.distinct bp_raw.inject} @{thms Alpha_lam.cases Alpha_bp.cases Compat_bp.cases} ctxt)) ctxt)) *}
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_inj}, []), (build_alpha_inj @{thms alpha_lam_raw_alpha_bp_raw.intros} @{thms lam_raw.distinct lam_raw.inject bp_raw.distinct bp_raw.inject} @{thms alpha_lam_raw.cases alpha_bp_raw.cases} ctxt)) ctxt)) *}
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding alpha_dis}, []), (flat (map (distinct_rel ctxt @{thms alpha_lam_raw.cases}) ([(@{thms lam_raw.distinct},@{term alpha_lam_raw})])))) ctxt)) *}
+local_setup {* (fn ctxt => snd (Local_Theory.note ((@{binding Alpha_dis}, []), (flat (map (distinct_rel ctxt @{thms Alpha_lam.cases}) ([(@{thms lam_raw.distinct},@{term Alpha_lam})])))) ctxt)) *}
+lemma "Alpha_lam x y = alpha_lam_raw x y"
+apply rule
+apply(induct x y rule: Alpha_lam_Alpha_bp_Compat_bp.inducts(1))
+apply(simp_all only: alpha_lam_raw_alpha_bp_raw.intros)
+apply(simp_all add: alpha_inj)
+apply(erule exE) apply(rule_tac x="pi" in exI)
+apply(simp add: alpha_gen)
+apply clarify
+apply simp
+defer
+apply(induct x y rule: alpha_lam_raw_alpha_bp_raw.inducts(1))
+apply(simp_all only: Alpha_lam_Alpha_bp_Compat_bp.intros)
+apply(simp_all add: Alpha_inj)
+apply(erule exE) apply(rule_tac x="pi" in exI)
+apply(simp add: alpha_gen)
+apply clarify
+apply simp
+oops
 
 lemma Test1:
   assumes "distinct [x, y]"