--- a/Nominal/Parser.thy	Fri Mar 19 15:01:01 2010 +0100
+++ b/Nominal/Parser.thy	Fri Mar 19 18:42:57 2010 +0100
@@ -306,7 +306,7 @@
   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, fv_def), ((alpha_ts, alpha_intros), (alpha_cases, alpha_induct))), lthy4) =
+  val ((((fv_ts, ordered_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_nobn, alpha_ts_bn) = chop (length perms) alpha_ts
@@ -325,7 +325,7 @@
   val (fv_bn_eqvts, lthy6a) =
     if fv_ts_bn = [] then ([], lthy6) else
     fold_map (build_bv_eqvt ((flat (map snd bv_eqvts)) @ fv_def @ raw_perm_def) inducts)
-      (fv_ts_bn ~~ (map snd bns)) lthy6;
+      (fv_ts_bn ~~ bn_nos) lthy6;
   val raw_fv_bv_eqvt = flat (map snd bv_eqvts) @ (snd fv_eqvts) @ flat (map snd fv_bn_eqvts)
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
@@ -365,12 +365,13 @@
     else constr_rsp_tac alpha_eq_iff (fv_rsp @ bns_rsp) alpha_equivp 1
   val (const_rsps, lthy12) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
     const_rsp_tac) (raw_consts @ alpha_ts_bn) lthy11
-  val qfv_names = map (unsuffix "_raw" o Long_Name.base_name o fst o dest_Const) fv_ts
-  val (qfv_defs, lthy12a) = fold_map Quotient_Def.quotient_lift_const (qfv_names ~~ fv_ts) lthy12;
+  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_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 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 (qalpha_ts_bn, qbn_defs, lthy12c) = quotient_lift_consts_export (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
@@ -381,6 +382,8 @@
   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);
+  fun note_suffix s th ctxt =
+    snd (Local_Theory.note ((suffix_bind s, []), th) ctxt);
   fun note_simp_suffix s th ctxt =
     snd (Local_Theory.note ((suffix_bind s, [Attrib.internal (K Simplifier.simp_add)]), th) ctxt);
   val (_, lthy14) = Local_Theory.note ((suffix_bind "induct",
@@ -413,9 +416,13 @@
   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))
-  val lthy22 = Class.prove_instantiation_instance tac lthy21 handle _ => lthy20
+  val lthy22 = Class.prove_instantiation_instance tac lthy21
+  val fv_alpha_all = combine_fv_alpha_bns (qfv_ts_nobn, qfv_ts_bn) (alpha_ts_nobn, qalpha_ts_bn) bn_nos;
+  val (names, supp_eq_t) = supp_eq fv_alpha_all;
+  val q_supp = HOLogic.conj_elims (Goal.prove lthy22 names [] supp_eq_t (fn _ => supp_eq_tac q_induct q_fv q_perm q_eq_iff lthy22 1)) handle _ => [];
+  val lthy23 = note_suffix "supp" q_supp lthy22;
 in
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy22)
+  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy23)
 end
 *}