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

--- a/Nominal/NewFv.thy	Fri Apr 30 10:04:24 2010 +0200
+++ b/Nominal/NewFv.thy	Fri Apr 30 10:31:32 2010 +0200
@@ -281,7 +281,7 @@
   val fv_bns_exp = map (Morphism.term morphism) fv_bns
 
 in
-  ((fv_frees_exp, fv_bns_exp), info, lthy'')
+  ((fv_frees_exp, fv_bns_exp), @{thms refl}, lthy'')
 end
 *}
 

--- a/Nominal/NewParser.thy	Fri Apr 30 10:04:24 2010 +0200
+++ b/Nominal/NewParser.thy	Fri Apr 30 10:31:32 2010 +0200
@@ -277,8 +277,9 @@
   val thy = Local_Theory.exit_global lthy2;
   val lthy3 = Theory_Target.init NONE thy;
 
-  val ((fv, fvbn), info, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
-  val (alpha, lthy5) = define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy4;
+  val ((fv, fvbn), fvsimps, lthy4) = define_raw_fv dtinfo bn_funs_decls raw_bclauses lthy3;
+  val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy5) =
+    define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy4;
 in
   ((raw_dt_names, raw_bn_funs_loc, raw_bn_eqs_loc, raw_bclauses, raw_bns), lthy5)
 end