--- a/Nominal/Lift.thy	Tue Mar 02 17:11:58 2010 +0100
+++ b/Nominal/Lift.thy	Tue Mar 02 17:48:41 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 =
@@ -48,9 +48,9 @@
 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,7 +64,7 @@
   "rbv5 rLnil = {}"
 | "rbv5 (rLcons n t ltl) = {atom n} \<union> (rbv5 ltl)"
 
-ML
+ML {*
 val thy1 = @{theory};
 val info = Datatype.the_info @{theory} "Lift.rtrm5"
 val number = 2;
@@ -73,7 +73,7 @@
 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;