--- a/Nominal/Lift.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Lift.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -7,7 +7,7 @@
 
 datatype rtrm2 =
   rVr2 "name"
-| rAp2 "rtrm2" "rtrm2"
+| rAp2 "rtrm2" "rtrm2 list"
 | rLt2 "ras" "rtrm2" --"bind (bv2 l) in (r)"
 and ras =
   rAs "name" "rtrm2"
@@ -45,6 +45,10 @@
              [[[], []]]  (*, [[], [[], []]] *) ];
 val bv_simps = @{thms rbv2.simps}
 val info = Datatype.the_info @{theory} ftname;
+*}
+
+.
+{*
 val descr = #descr info;
 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
 val full_tnames = List.take (all_full_tnames, length tnames);