--- a/Nominal/Parser.thy	Thu Mar 18 00:17:21 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 18 07:26:36 2010 +0100
@@ -1,5 +1,5 @@
 theory Parser
-imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Perm" "Fv" "Rsp"
+imports "Nominal2_Atoms" "Nominal2_Eqvt" "Nominal2_Supp" "Perm" "Fv" "Rsp" "Lift"
 begin
 
 atom_decl name
@@ -253,14 +253,6 @@
 end
 *}
 
-ML {*
-fun un_raw name = unprefix "_raw" name handle Fail _ => name
-fun add_under names = hd names :: (map (prefix "_") (tl names))
-fun un_raws name = implode (map un_raw (add_under (space_explode "_" name)))
-val un_raw_names = rename_vars un_raws
-fun lift_thm ctxt thm = un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm)))
-*}
-
 lemma equivp_hack: "equivp x"
 sorry
 ML {*
@@ -333,10 +325,11 @@
   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;
-  val alpha_intros = #intrs alpha;
+  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 alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distincts) alpha_cases_loc lthy4
+  val alpha_inj_loc = build_alpha_inj alpha_intros_loc (inject @ distincts) alpha_cases_loc lthy4
   val alpha_inj = ProofContext.export lthy4 lthy3 alpha_inj_loc
   val _ = tracing "Proving equivariance";
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
@@ -350,18 +343,16 @@
       (fv_ts_loc_bn ~~ (map snd bns)) lthy6;
   val lthy6 = lthy6a;
   val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
-  val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
+  val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy2 raw_fv_bv_eqvt_loc;
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
-    else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc @ raw_fv_bv_eqvt_loc) lthy6 1
-  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc alpha_eqvt_tac' lthy6;
-  val alpha_eqvt = ProofContext.export lthy6 lthy2 alpha_eqvt_loc;
+    else alpha_eqvt_tac alpha_induct (raw_perm_def @ alpha_inj @ raw_fv_bv_eqvt) lthy6 1
+  val alpha_eqvt = build_alpha_eqvts alpha_ts alpha_eqvt_tac' lthy6;
   val _ = tracing "Proving equivalence";
-  val alpha_equivp_loc = 
-    if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_loc_nobn
-    else build_equivps alpha_ts_loc induct alpha_induct_loc
-      inject alpha_inj_loc distincts alpha_cases_loc alpha_eqvt_loc lthy6;
-  val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
+  val alpha_equivp =
+    if !cheat_equivp then map (equivp_hack lthy6) alpha_ts_nobn
+    else build_equivps alpha_ts induct alpha_induct
+      inject alpha_inj distincts alpha_cases alpha_eqvt lthy6;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
@@ -374,10 +365,7 @@
       map (fn (cname, dts) =>
         Const (cname, map (typ_of_dtyp descr sorts) dts --->
           typ_of_dtyp descr sorts (DtRec i))) l) descr);
-  val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7;
-  val (consts_loc, const_defs) = split_list consts_defs;
-  val morphism_8_7 = ProofContext.export_morphism lthy8 lthy7;
-  val consts = map (Morphism.term morphism_8_7) consts_loc;
+  val (consts, const_defs, lthy8) = quotient_lift_consts_export (const_names ~~ raw_consts) lthy7;
   (* Could be done nicer *)
   val q_tys = distinct (op =) (map (snd o strip_type o fastype_of) consts);
   val _ = tracing "Proving respects";