--- a/Nominal/Lift.thy	Mon Mar 01 16:04:03 2010 +0100
+++ b/Nominal/Lift.thy	Mon Mar 01 21:50:24 2010 +0100
@@ -64,6 +64,8 @@
   "rbv5 rLnil = {}"
 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
 
+ML Typedef.add_typedef
+
 ML {*
 val thy1 = @{theory};
 val info = Datatype.the_info @{theory} "Lift.rtrm5"
@@ -135,9 +137,13 @@
 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 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;
 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 lthy12 = snd (Local_Theory.note ((@{binding lift_induct}, []), [lift_induct]) lthy11);
 *}
 
 setup {* fn _ => Local_Theory.exit_global lthy12 *}