--- a/Nominal/Lift.thy	Sat Mar 27 14:38:22 2010 +0100
+++ b/Nominal/Lift.thy	Sat Mar 27 14:55:07 2010 +0100
@@ -55,18 +55,18 @@
 *}
 
 ML {*
-fun lift_thm ctxt thm =
+fun lift_thm qtys ctxt thm =
 let
   val un_raw_names = rename_vars un_raws
 in
-  rename_thm_bvars (un_raw_names (snd (Quotient_Tacs.lifted_attrib (Context.Proof ctxt, thm))))
+  rename_thm_bvars (un_raw_names (Quotient_Tacs.lifted qtys ctxt thm))
 end
 *}
 
 ML {*
-fun quotient_lift_consts_export spec ctxt =
+fun quotient_lift_consts_export qtys spec ctxt =
 let
-  val (result, ctxt') = fold_map Quotient_Def.quotient_lift_const spec ctxt;
+  val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt;
   val (ts_loc, defs_loc) = split_list result;
   val morphism = ProofContext.export_morphism ctxt' ctxt;
   val ts = map (Morphism.term morphism) ts_loc

--- a/Nominal/Parser.thy	Sat Mar 27 14:38:22 2010 +0100
+++ b/Nominal/Parser.thy	Sat Mar 27 14:55:07 2010 +0100
@@ -390,57 +390,57 @@
   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
-  val (q_tys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6;
+  val (qtys, lthy7) = define_quotient_types qty_binds all_typs alpha_ts_nobn alpha_equivp lthy6;
   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
   val raw_consts =
     flat (map (fn (i, (_, _, l)) =>
       map (fn (cname, dts) =>
         Const (cname, map (typ_of_dtyp descr sorts) dts --->
           typ_of_dtyp descr sorts (DtRec i))) l) descr);
-  val (consts, const_defs, lthy8) = quotient_lift_consts_export (const_names ~~ raw_consts) lthy7;
+  val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
   val _ = tracing "Proving respects";
   val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;
   val _ = map tracing (map PolyML.makestring bns_rsp_pre')
   val (bns_rsp_pre, lthy9) = fold_map (
-    fn (bn_t, i) => prove_const_rsp Binding.empty [bn_t] (fn _ =>
+    fn (bn_t, i) => prove_const_rsp qtys Binding.empty [bn_t] (fn _ =>
        resolve_tac bns_rsp_pre' 1)) bns lthy8;
   val bns_rsp = flat (map snd bns_rsp_pre);
   fun fv_rsp_tac _ = if !cheat_fv_rsp then Skip_Proof.cheat_tac thy
     else fvbv_rsp_tac alpha_induct fv_def lthy8 1;
   val fv_rsps = prove_fv_rsp fv_alpha_all alpha_ts fv_rsp_tac lthy9;
   val (fv_rsp_pre, lthy10) = fold_map
-    (fn fv => fn ctxt => prove_const_rsp Binding.empty [fv]
+    (fn fv => fn ctxt => prove_const_rsp qtys Binding.empty [fv]
     (fn _ => asm_simp_tac (HOL_ss addsimps fv_rsps) 1) ctxt) fv_ts lthy9;
   val fv_rsp = flat (map snd fv_rsp_pre);
-  val (perms_rsp, lthy11) = prove_const_rsp Binding.empty perms
+  val (perms_rsp, lthy11) = prove_const_rsp qtys Binding.empty perms
     (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy10;
   val alpha_bn_rsp_pre = prove_alpha_bn_rsp alpha_ts alpha_induct (alpha_eq_iff @ rel_dists @ rel_dists_bn) alpha_equivp exhausts alpha_ts_bn lthy11;
-  val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
+  val (alpha_bn_rsps, lthy11a) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
         (fn _ => asm_simp_tac (HOL_ss addsimps alpha_bn_rsp_pre) 1)) alpha_ts_bn lthy11
 (*  val _ = map tracing (map PolyML.makestring alpha_bn_rsps);*)
   fun const_rsp_tac _ =
     if !cheat_const_rsp then Skip_Proof.cheat_tac thy
     else let val alpha_alphabn = prove_alpha_alphabn alpha_ts alpha_induct alpha_eq_iff alpha_ts_bn lthy11a
       in constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp @ reflps @ alpha_alphabn) 1 end
-  val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
+  val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp qtys Binding.empty [cnst]
     const_rsp_tac) raw_consts lthy11a
   val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) ordered_fv_ts
-  val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export (qfv_names ~~ ordered_fv_ts) lthy12;
+  val (qfv_ts, qfv_defs, lthy12a) = quotient_lift_consts_export qtys (qfv_names ~~ ordered_fv_ts) lthy12;
   val (qfv_ts_nobn, qfv_ts_bn) = chop (length perms) qfv_ts;
   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 (qbn_ts, qbn_defs, lthy12b) = quotient_lift_consts_export qtys (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 (qalpha_ts_bn, qbn_defs, lthy12c) = quotient_lift_consts_export (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
+  val (qalpha_ts_bn, qalphabn_defs, lthy12c) = quotient_lift_consts_export qtys (qalpha_bn_names ~~ alpha_ts_bn) lthy12b;
   val _ = tracing "Lifting permutations";
   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;
+  val thy' = define_lifted_perms qtys qty_full_names (perm_names ~~ perms) raw_perm_simps thy;
   val lthy13 = Theory_Target.init NONE thy';
   val q_name = space_implode "_" qty_names;
   fun suffix_bind s = Binding.qualify true q_name (Binding.name s);
   val _ = tracing "Lifting induction";
   val constr_names = map (Long_Name.base_name o fst o dest_Const) consts;
-  val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 induct);
+  val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 induct);
   fun note_suffix s th ctxt =
     snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
   fun note_simp_suffix s th ctxt =
@@ -449,27 +449,27 @@
     [Attrib.internal (K (Rule_Cases.case_names constr_names))]), [Rule_Cases.name constr_names q_induct]) lthy13;
   val q_inducts = Project_Rule.projects lthy13 (1 upto (length alpha_inducts)) q_induct
   val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14;
-  val q_perm = map (lift_thm lthy14) raw_perm_def;
+  val q_perm = map (lift_thm qtys lthy14) raw_perm_def;
   val lthy15 = note_simp_suffix "perm" q_perm lthy14a;
-  val q_fv = map (lift_thm lthy15) fv_def;
+  val q_fv = map (lift_thm qtys lthy15) fv_def;
   val lthy16 = note_simp_suffix "fv" q_fv lthy15;
-  val q_bn = map (lift_thm lthy16) raw_bn_eqs;
+  val q_bn = map (lift_thm qtys lthy16) raw_bn_eqs;
   val lthy17 = note_simp_suffix "bn" q_bn lthy16;
   val _ = tracing "Lifting eq-iff";
   val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms alphas2}) alpha_eq_iff
   val eq_iff_unfolded2 = map (Local_Defs.unfold lthy17 @{thms alphas}) eq_iff_unfolded1
-  val q_eq_iff_pre1 = map (lift_thm lthy17) eq_iff_unfolded2;
+  val q_eq_iff_pre1 = map (lift_thm qtys lthy17) eq_iff_unfolded2;
   val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas2}) q_eq_iff_pre1
   val q_eq_iff = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre2
   val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17;
-  val q_dis = map (lift_thm lthy18) rel_dists;
+  val q_dis = map (lift_thm qtys lthy18) rel_dists;
   val lthy19 = note_simp_suffix "distinct" q_dis lthy18;
-  val q_eqvt = map (lift_thm lthy19) (bv_eqvt @ fv_eqvt);
+  val q_eqvt = map (lift_thm qtys lthy19) (bv_eqvt @ fv_eqvt);
   val (_, lthy20) = Local_Theory.note ((Binding.empty,
     [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19;
   val _ = tracing "Finite Support";
   val supports = map (prove_supports lthy20 q_perm) consts;
-  val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports q_tys);
+  val fin_supp = HOLogic.conj_elims (prove_fs lthy20 q_induct supports qtys);
   val thy3 = Local_Theory.exit_global lthy20;
   val lthy21 = Theory_Target.instantiation (qty_full_names, [], @{sort fs}) thy3;
   fun tac _ = Class.intro_classes_tac [] THEN (ALLGOALS (resolve_tac fin_supp))

--- a/Nominal/Perm.thy	Sat Mar 27 14:38:22 2010 +0100
+++ b/Nominal/Perm.thy	Sat Mar 27 14:55:07 2010 +0100
@@ -9,6 +9,19 @@
 *}
 
 ML {*
+fun quotient_lift_consts_export qtys spec ctxt =
+let
+  val (result, ctxt') = fold_map (Quotient_Def.quotient_lift_const qtys) spec ctxt;
+  val (ts_loc, defs_loc) = split_list result;
+  val morphism = ProofContext.export_morphism ctxt' ctxt;
+  val ts = map (Morphism.term morphism) ts_loc
+  val defs = Morphism.fact morphism defs_loc
+in
+  (ts, defs, ctxt')
+end
+*}
+
+ML {*
 fun prove_perm_empty lthy induct perm_def perm_frees =
 let
   val perm_types = map fastype_of perm_frees;
@@ -118,12 +131,12 @@
 *}
 
 ML {*
-fun define_lifted_perms full_tnames name_term_pairs thms thy =
+fun define_lifted_perms qtys full_tnames name_term_pairs thms thy =
 let
   val lthy =
     Theory_Target.instantiation (full_tnames, [], @{sort pt}) thy;
-  val lthy' = fold (snd oo Quotient_Def.quotient_lift_const) name_term_pairs lthy
-  val lifted_thms = map (fn x => snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy', x))) thms
+  val (_, _, lthy') = quotient_lift_consts_export qtys name_term_pairs lthy;
+  val lifted_thms = map (Quotient_Tacs.lifted qtys lthy') thms;
   fun tac _ =
     Class.intro_classes_tac [] THEN
     (ALLGOALS (resolve_tac lifted_thms))

--- a/Nominal/Rsp.thy	Sat Mar 27 14:38:22 2010 +0100
+++ b/Nominal/Rsp.thy	Sat Mar 27 14:55:07 2010 +0100
@@ -3,9 +3,9 @@
 begin
 
 ML {*
-fun const_rsp lthy const =
+fun const_rsp qtys lthy const =
 let
-  val nty = fastype_of (Quotient_Term.quotient_lift_const ("", const) lthy)
+  val nty = fastype_of (Quotient_Term.quotient_lift_const qtys ("", const) lthy)
   val rel = Quotient_Term.equiv_relation_chk lthy (fastype_of const, nty);
 in
   HOLogic.mk_Trueprop (rel $ const $ const)
@@ -39,9 +39,9 @@
 *}
 
 ML {*
-fun prove_const_rsp bind consts tac ctxt =
+fun prove_const_rsp qtys bind consts tac ctxt =
 let
-  val rsp_goals = map (const_rsp ctxt) consts
+  val rsp_goals = map (const_rsp qtys ctxt) consts
   val thy = ProofContext.theory_of ctxt
   val (fixed, user_goals) = split_list (map (get_rsp_goal thy) rsp_goals)
   val fixed' = distinct (op =) (flat fixed)