diff -r e965524c3301 -r 003c7e290a04 Nominal/Lift.thy
--- a/Nominal/Lift.thy	Tue Mar 02 15:05:50 2010 +0100
+++ b/Nominal/Lift.thy	Tue Mar 02 15:07:27 2010 +0100
@@ -25,7 +25,7 @@
 val ntnames = [@{binding trm2}, @{binding as}]
 val ncnames = ["Vr2", "Ap2", "Lt2", "As"] *} *)
 
-(* datatype rkind =
+datatype rkind =
     Type
   | KPi "rty" "name" "rkind"
 and rty =
@@ -41,16 +41,16 @@
 val thy1 = @{theory};
 val info = Datatype.the_info @{theory} "Lift.rkind"
 val number = 3;
-val binds =  [[ [], [[], [(NONE, 1)], [(NONE, 1)]] ],
-   [ [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]] ],
-   [ [[]], [[]], [[], []], [[], [(NONE, 1)], [(NONE, 1)]]]];
+val binds = [[ [], [(NONE, 1, 2)]],
+   [ [], [], [(NONE, 1, 2)] ],
+   [ [], [], [], [(NONE, 1, 2)]]];
 val bvs = []
 val bv_simps = []
 
 val ntnames = [@{binding kind}, @{binding ty}, @{binding trm}]
-val ncnames = ["TYP", "KPI", "TCONST", "TAPP", "TPI", "CONST", "VAR", "APP", "LAM"]*} *)
+val ncnames = ["TYP", "KPI", "TCONST", "TAPP", "TPI", "CONST", "VAR", "APP", "LAM"]
 
-datatype rtrm5 =
+(*datatype rtrm5 =
   rVr5 "name"
 | rAp5 "rtrm5" "rtrm5"
 | rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
@@ -64,18 +64,17 @@
   "rbv5 rLnil = {}"
 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
 
-ML Typedef.add_typedef
-
-ML {*
+ML
 val thy1 = @{theory};
 val info = Datatype.the_info @{theory} "Lift.rtrm5"
 val number = 2;
-val binds = [ [[[]], [[], []], [[(SOME @{term rbv5}, 0)], [(SOME @{term rbv5}, 0)]]], [[], [[], [], []]]  ]
+val binds = [ [[], [], [(SOME @{term rbv5}, 0, 1)]], [[], []]  ]
 val bvs = [(@{term rbv5}, 1)]
 val bv_simps = @{thms rbv5.simps}
 
 val ntnames = [@{binding trm5}, @{binding lts}]
-val ncnames = ["Vr5", "Ap5", "Lt5", "Lnil", "Lcons"]
+val ncnames = ["Vr5", "Ap5", "Lt5", "Lnil", "Lcons"]*)
+
 
 val descr = #descr info;
 val sorts = #sorts info;
@@ -113,7 +112,7 @@
 val (bv_eqvts, lthy3) = fold_map build_bv_eqvt bvs lthy2;
 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_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 = ProofContext.export lthy4 lthy1 alpha_equivp_loc
 val lthy5 = define_quotient_type
@@ -126,19 +125,19 @@
         typ_of_dtyp descr sorts (DtRec i))) l) descr);
 val (csdefl, lthy6) = fold_map Quotient_Def.quotient_lift_const (ncnames ~~ consts) lthy5;
 val (cs, def) = split_list csdefl;
-val ((_, fv_rsp), lthy7) = prove_const_rsp Binding.empty fv_ts
-  (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy6
-val (bvs_rsp', lthy8) = fold_map (
+val (bvs_rsp', lthy7) = fold_map (
   fn (bv_t, i) => prove_const_rsp Binding.empty [bv_t]
-    (fn _ => fvbv_rsp_tac (nth alpha_inducts i) bv_simps 1)) bvs lthy7
-val bvs_rsp = flat (map snd bvs_rsp')
+    (fn _ => fvbv_rsp_tac (nth alpha_inducts i) bv_simps 1)) bvs lthy6;
+val ((_, fv_rsp), lthy8) = prove_const_rsp Binding.empty fv_ts
+  (fn _ => fvbv_rsp_tac alpha_induct fv_def 1) lthy7;
+val bvs_rsp = flat (map snd bvs_rsp');
 val (const_rsps, lthy9) = fold_map (fn cnst => prove_const_rsp Binding.empty [cnst]
   (fn _ => constr_rsp_tac alpha_inj (fv_rsp @ bvs_rsp) alpha_equivp 1)) consts lthy8
 val (perms_rsp, lthy10) = prove_const_rsp Binding.empty perms
   (fn _ => asm_simp_tac (HOL_ss addsimps alpha_eqvt) 1) lthy9;
 val thy3 = Local_Theory.exit_global lthy10;
 (* TODO: fix this hack... *)
-val tinfo = #abs_type (Typedef.the_info thy3 "Lift.trm5");
+(*val tinfo = #abs_type (Typedef.the_info thy3 "Lift.trm5");*)
 (*val thy4 = define_lifted_perms ["Term1.trm1"] [("permute_trm1", @{term "permute :: perm \<Rightarrow> rtrm1 \<Rightarrow> rtrm1"})]
   @{thms permute_rtrm1_permute_bp_zero permute_rtrm1_permute_bp_append}*)
 val lthy11 = Theory_Target.init NONE thy3;