--- a/Nominal/Lift.thy	Fri Feb 26 16:22:47 2010 +0100
+++ b/Nominal/Lift.thy	Fri Feb 26 18:21:39 2010 +0100
@@ -5,7 +5,7 @@
 atom_decl name
 atom_decl ident
 
-datatype rtrm2 =
+(* datatype rtrm2 =
   rVr2 "name"
 | rAp2 "rtrm2" "rtrm2"
 | rLt2 "ras" "rtrm2" --"bind (bv2 l) in (r)"
@@ -13,7 +13,6 @@
   rAs "name" "rtrm2"
 
 primrec rbv2 where "rbv2 (rAs x t) = {atom x}"
-
 ML {*
 val thy1 = @{theory};
 val info = Datatype.the_info @{theory} "Lift.rtrm2"
@@ -24,10 +23,57 @@
 val bv_simps = @{thms rbv2.simps}
 
 val ntnames = [@{binding trm2}, @{binding as}]
-val ncnames = ["Vr2", "Ap2", "Lt2", "As"]
+val ncnames = ["Vr2", "Ap2", "Lt2", "As"] *} *)
+
+(* datatype rkind =
+    Type
+  | KPi "rty" "name" "rkind"
+and rty =
+    TConst "ident"
+  | TApp "rty" "rtrm"
+  | TPi "rty" "name" "rty"
+and rtrm =
+    Const "ident"
+  | Var "name"
+  | App "rtrm" "rtrm"
+  | Lam "rty" "name" "rtrm"
+ML {*
+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 bvs = []
+val bv_simps = []
 
+val ntnames = [@{binding kind}, @{binding ty}, @{binding trm}]
+val ncnames = ["TYP", "KPI", "TCONST", "TAPP", "TPI", "CONST", "VAR", "APP", "LAM"]*} *)
 
+datatype rtrm5 =
+  rVr5 "name"
+| rAp5 "rtrm5" "rtrm5"
+| rLt5 "rlts" "rtrm5" --"bind (bv5 lts) in (rtrm5)"
+and rlts =
+  rLnil
+| rLcons "name" "rtrm5" "rlts"
 
+primrec
+  rbv5
+where
+  "rbv5 rLnil = {}"
+| "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
+
+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 bvs = [(@{term rbv5}, 1)]
+val bv_simps = @{thms rbv5.simps}
+
+val ntnames = [@{binding trm5}, @{binding lts}]
+val ncnames = ["Vr5", "Ap5", "Lt5", "Lnil", "Lcons"]
 
 val descr = #descr info;
 val sorts = #sorts info;
@@ -88,11 +134,13 @@
   (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 lift_induct = snd (Quotient_Tacs.lifted_attrib (Context.Proof lthy1, induct));
-val lthy11 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy10)
+val thy3 = Local_Theory.exit_global lthy10;
+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)
 *}
 
-setup {* fn _ => Local_Theory.exit_global lthy11 *}
+setup {* fn _ => Local_Theory.exit_global lthy12 *}
 thm lift_induct
 
 end