--- a/Nominal/Lift.thy	Sun Mar 07 21:30:12 2010 +0100
+++ b/Nominal/Lift.thy	Sun Mar 07 21:30:57 2010 +0100
@@ -64,6 +64,8 @@
   "rbv5 rLnil = {}"
 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
 
+
+
 ML {*
 val thy1 = @{theory};
 val info = Datatype.the_info @{theory} "Lift.rtrm5"
@@ -85,21 +87,24 @@
 val induct = #induct info;
 val inducts = #inducts info;
 val infos = map (Datatype.the_info thy1) all_full_tnames;
+val rel_infos = List.take (infos, number);
 val inject = flat (map #inject infos);
 val distinct = flat (map #distinct infos);
+val rel_distinct = map #distinct rel_infos;
 val ((raw_perm_def, raw_perm_simps, perms), thy2) = define_raw_perms info number thy1;
 val lthy1 = Theory_Target.init NONE thy2
 val (((fv_ts_loc, fv_def_loc), alpha), lthy2) = define_fv_alpha info binds lthy1;
 val alpha_ts_loc = #preds alpha
 val alpha_intros = #intrs alpha
-val alpha_cases = #elims alpha
+val alpha_cases_loc = #elims alpha
 val alpha_induct_loc = #induct alpha
+val alpha_cases = ProofContext.export lthy2 lthy1 alpha_cases_loc
 val [alpha_induct] = ProofContext.export lthy2 lthy1 [alpha_induct_loc]
 (* TODO replace when inducts is provided by the 2 lines below: *)
 val alpha_inducts = Project_Rule.projects lthy2 (1 upto number) alpha_induct
 (*val alpha_inducts_loc = #inducts alpha
 val alpha_inducts = ProofContext.export lthy2 lthy1 alpha_inducts_loc*)
-val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases lthy2
+val alpha_inj_loc = build_alpha_inj alpha_intros (inject @ distinct) alpha_cases_loc lthy2
 val alpha_inj = ProofContext.export lthy2 lthy1 alpha_inj_loc
 val fv_def = ProofContext.export lthy2 lthy1 fv_def_loc
 val morphism = ProofContext.export_morphism lthy2 lthy1
@@ -109,7 +114,7 @@
 val (fv_eqvts, lthy4) = build_eqvts Binding.empty fv_ts_loc perms (fv_def_loc @ raw_perm_def) induct lthy3;
 val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc perms (raw_perm_def @ alpha_inj_loc) alpha_induct_loc lthy4;
 val alpha_eqvt = ProofContext.export lthy4 lthy1 alpha_eqvt_loc;
-val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc inject alpha_inj_loc distinct alpha_cases alpha_eqvt_loc lthy4;
+val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy4;
 val alpha_equivp = ProofContext.export lthy4 lthy1 alpha_equivp_loc
 val lthy5 = define_quotient_type
   (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((ntnames ~~ typs) ~~ alpha_ts))
@@ -139,10 +144,13 @@
 val lthy11 = Theory_Target.init NONE thy3;
 val lift_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy11, induct));
 val lthy12 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy11);
+val rel_dists = flat (map (distinct_rel lthy12 alpha_cases) (rel_distinct ~~ (List.take (alpha_ts, number))))
+
 *}
 
 setup {* fn _ => Local_Theory.exit_global lthy12 *}
 thm lift_induct
 
+
 end