--- a/Quot/Nominal/Fv.thy	Fri Feb 19 12:05:58 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Fri Feb 19 16:45:24 2010 +0100
@@ -215,23 +215,39 @@
 print_theorems
 *)
 
+
 ML {*
-fun build_alpha_inj_gl thms ctxt =
+fun alpha_inj_tac dist_inj intrs elims =
+  SOLVED' (asm_full_simp_tac (HOL_ss addsimps intrs)) ORELSE'
+  rtac @{thm iffI} THEN' RANGE [
+     (eresolve_tac elims THEN_ALL_NEW
+       asm_full_simp_tac (HOL_ss addsimps dist_inj)
+     ),
+     (asm_full_simp_tac (HOL_ss addsimps intrs))]
+*}
+
+ML {*
+fun build_alpha_inj_gl thm =
+  let
+    val prop = prop_of thm;
+    val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
+    val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
+    fun list_conj l = foldr1 HOLogic.mk_conj l;
+  in
+    if hyps = [] then concl
+    else HOLogic.mk_eq (concl, list_conj hyps)
+  end;
+*}
+
+ML {*
+fun build_alpha_inj intrs dist_inj elims ctxt =
 let
-  (* TODO: use the context for export *)
-  val ((_, thms_imp), ctxt') = Variable.import false thms ctxt;
-  fun inj_thm thm_imp =
-    let
-      val prop = prop_of thm_imp;
-      val concl = HOLogic.dest_Trueprop (Logic.strip_imp_concl prop);
-      val hyps = map HOLogic.dest_Trueprop (Logic.strip_imp_prems prop);
-      fun list_conj l = foldr1 HOLogic.mk_conj l;
-    in
-      if hyps = [] then concl
-      else HOLogic.mk_eq (concl, list_conj hyps)
-    end;
+  val ((_, thms_imp), ctxt') = Variable.import false intrs ctxt;
+  val gls = map (HOLogic.mk_Trueprop o build_alpha_inj_gl) thms_imp;
+  fun tac _ = alpha_inj_tac dist_inj intrs elims 1;
+  val thms = map (fn gl => Goal.prove ctxt' [] [] gl tac) gls;
 in
-  Logic.mk_conjunction_list (map (HOLogic.mk_Trueprop o inj_thm) thms_imp)
+  Variable.export ctxt' ctxt thms
 end
 *}