# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1272616354 -7200
# Node ID bc075a4ef02f0d157e6e5e60c52a5333229f4649
# Parent  953f74f407277ea32ff6e38dc4c05390923371d7# Parent  652f310f0dbac9d1301a0c7ef6a2c51ee0901d5c
merge

diff -r 652f310f0dba -r bc075a4ef02f Nominal/NewAlpha.thy
--- a/Nominal/NewAlpha.thy	Fri Apr 30 10:09:45 2010 +0100
+++ b/Nominal/NewAlpha.thy	Fri Apr 30 10:32:34 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
 *}
 
diff -r 652f310f0dba -r bc075a4ef02f Nominal/NewFv.thy
--- a/Nominal/NewFv.thy	Fri Apr 30 10:09:45 2010 +0100
+++ b/Nominal/NewFv.thy	Fri Apr 30 10:32:34 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
 *}
 
diff -r 652f310f0dba -r bc075a4ef02f Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Fri Apr 30 10:09:45 2010 +0100
+++ b/Nominal/NewParser.thy	Fri Apr 30 10:32:34 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