--- a/Quot/Nominal/Fv.thy	Thu Feb 18 18:33:53 2010 +0100
+++ b/Quot/Nominal/Fv.thy	Fri Feb 19 10:17:35 2010 +0100
@@ -215,4 +215,24 @@
 print_theorems
 *)
 
+ML {*
+fun build_alpha_inj_gl thms 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;
+in
+  Logic.mk_conjunction_list (map (HOLogic.mk_Trueprop o inj_thm) thms_imp)
 end
+*}
+
+end

--- a/Quot/Nominal/Terms.thy	Thu Feb 18 18:33:53 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Fri Feb 19 10:17:35 2010 +0100
@@ -1,5 +1,5 @@
 theory Terms
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Abs" "Perm" "Fv" "../../Attic/Prove"
 begin
 
 atom_decl name
@@ -38,6 +38,9 @@
   alpha_bp ("_ \<approx>1b _" [100, 100] 100)
 thm alpha_rtrm1_alpha_bp.intros
 
+prove {* build_alpha_inj_gl @{thms alpha_rtrm1_alpha_bp.intros} @{context} *}
+sorry
+
 lemma alpha1_inj:
 "(rVr1 a \<approx>1 rVr1 b) = (a = b)"
 "(rAp1 t1 s1 \<approx>1 rAp1 t2 s2) = (t1 \<approx>1 t2 \<and> s1 \<approx>1 s2)"