--- a/Nominal/NewAlpha.thy	Fri Apr 30 10:04:24 2010 +0200
+++ b/Nominal/NewAlpha.thy	Fri Apr 30 10:31:32 2010 +0200
@@ -241,8 +241,19 @@
      {quiet_mode = true, verbose = false, alt_name = Binding.empty,
       coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
      all_alpha_names [] all_alpha_eqs [] lthy
+
+  val alpha_ts_loc = #preds alphas;
+  val alpha_induct_loc = #induct alphas;
+  val alpha_intros_loc = #intrs alphas;
+  val alpha_cases_loc = #elims alphas;
+  val morphism = ProofContext.export_morphism lthy' lthy;
+
+  val alpha_ts = map (Morphism.term morphism) alpha_ts_loc;
+  val alpha_induct = Morphism.thm morphism alpha_induct_loc;
+  val alpha_intros = Morphism.fact morphism alpha_intros_loc
+  val alpha_cases = Morphism.fact morphism alpha_cases_loc
 in
-  (alphas, lthy')
+  (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy')
 end
 *}