--- 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