--- a/Nominal/Lift.thy	Thu Mar 18 07:43:44 2010 +0100
+++ b/Nominal/Lift.thy	Thu Mar 18 08:03:42 2010 +0100
@@ -27,5 +27,26 @@
 end
 *}
 
+ML {*
+fun define_fv_alpha_export dt binds bns ctxt =
+let
+  val (((fv_ts_loc, fv_def_loc), alpha), ctxt') =
+    define_fv_alpha dt binds bns ctxt;
+  val alpha_ts_loc = #preds alpha
+  val alpha_induct_loc = #induct alpha
+  val alpha_intros_loc = #intrs alpha;
+  val alpha_cases_loc = #elims alpha
+  val morphism = ProofContext.export_morphism ctxt' ctxt;
+  val fv_ts = map (Morphism.term morphism) fv_ts_loc;
+  val fv_def = Morphism.fact morphism fv_def_loc;
+  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
+  (((fv_ts, fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), ctxt')
+end;
+*}
+
 end
 

--- a/Nominal/Parser.thy	Thu Mar 18 07:43:44 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 18 08:03:42 2010 +0100
@@ -289,9 +289,9 @@
   val morphism_2_1 = ProofContext.export_morphism lthy2 lthy
   val raw_bns_exp = map (apsnd (map (apfst (Morphism.term morphism_2_1)))) raw_bns;
   val bn_funs_decls = flat (map (fn (ith, l) => map (fn (bn, data) => (bn, ith, data)) l) raw_bns_exp);
-
   val raw_bn_funs = map (Morphism.term morphism_2_1) raw_bn_funs_loc
   val raw_bn_eqs = ProofContext.export lthy2 lthy raw_bn_eqs_loc
+
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names);
   val descr = #descr dtinfo;
   val sorts = #sorts dtinfo;
@@ -308,27 +308,15 @@
   val ((raw_perm_def, raw_perm_simps, perms), lthy3) =
     Local_Theory.theory_result (define_raw_perms dtinfo (length dts)) lthy2;
   val raw_binds_flat = map (map flat) raw_binds;
-  val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3;
-  val alpha_ts_loc = #preds alpha
-  val alpha_ts_loc_nobn = List.take (alpha_ts_loc, length perms)
-  val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3;
-  val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc;
-  val (fv_ts_loc_nobn, fv_ts_loc_bn) = chop (length perms) fv_ts_loc;
+  val (((fv_ts, fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) =
+    define_fv_alpha_export dtinfo raw_binds_flat bn_funs_decls lthy3;
   val (fv_ts_nobn, fv_ts_bn) = chop (length perms) fv_ts;
-  val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc;
   val (alpha_ts_nobn, alpha_ts_bn) = chop (length perms) alpha_ts
-  val alpha_induct_loc = #induct alpha
-  val [alpha_induct] = ProofContext.export lthy4 lthy3 [alpha_induct_loc];
   val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct
-  val fv_def = ProofContext.export lthy4 lthy3 fv_def_loc;
   val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo);
   val bn_tys = map (domain_type o fastype_of) raw_bn_funs;
   val bn_nos = map (dtyp_no_of_typ dts_names) bn_tys;
-  val bns = raw_bn_funs ~~ bn_nos; (* Are exported *)
-  val alpha_intros_loc = #intrs alpha;
-  val alpha_cases_loc = #elims alpha
-  val alpha_intros = ProofContext.export lthy4 lthy3 alpha_intros_loc
-  val alpha_cases = ProofContext.export lthy4 lthy3 alpha_cases_loc
+  val bns = raw_bn_funs ~~ bn_nos;
   val alpha_eq_iff = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases lthy4
   val _ = tracing "Proving equivariance";
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
@@ -384,8 +372,8 @@
   val qbn_names = map (fn (b, _ , _) => Name.of_binding b) bn_funs
   val (qbn_defs, lthy12b) = fold_map Quotient_Def.quotient_lift_const (qbn_names ~~ raw_bn_funs) lthy12a;
   val qalpha_bn_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) alpha_ts_bn
+  val (qbn_defs, lthy12c) = fold_map Quotient_Def.quotient_lift_const (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
   val _ = tracing "Lifting permutations";
-  val (qbn_defs, lthy12c) = fold_map Quotient_Def.quotient_lift_const (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
   val thy = Local_Theory.exit_global lthy12c;
   val perm_names = map (fn x => "permute_" ^ x) qty_names
   val thy' = define_lifted_perms qty_full_names (perm_names ~~ perms) raw_perm_simps thy;