--- a/Nominal/Ex/Lambda.thy	Sat Aug 21 16:20:10 2010 +0800
+++ b/Nominal/Ex/Lambda.thy	Sat Aug 21 17:55:42 2010 +0800
@@ -3,12 +3,14 @@
 begin
 
 atom_decl name
-declare [[STEPS = 20]]
+declare [[STEPS = 2]]
 
-nominal_datatype  lam =
+nominal_datatype 'a lam =
   Var "name"
-| App "lam" "lam"
-| Lam x::"name" l::"lam"  bind x in l
+| App "'a lam" "'a lam"
+| Lam x::"name" l::"'a lam"  bind x in l
+
+ML {* Datatype.read_typ *}
 
 
 thm eq_iff

--- a/Nominal/NewParser.thy	Sat Aug 21 16:20:10 2010 +0800
+++ b/Nominal/NewParser.thy	Sat Aug 21 17:55:42 2010 +0800
@@ -247,7 +247,7 @@
 (* for testing porposes - to exit the procedure early *)
 exception TEST of Proof.context
 
-val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 10);
+val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 0);
 
 fun get_STEPS ctxt = Config.get ctxt STEPS
 *}
@@ -626,7 +626,7 @@
   val thy = ProofContext.theory_of lthy
   
   fun mk_type full_tname tvrs =
-    Type (full_tname, map (fn a => TVar ((a, 0), [])) tvrs)
+    Type (full_tname, map (fn a => TFree (a, @{sort "{pt, fs}"})) tvrs)
 
   fun prep_cnstr full_tname tvs (cname, anno_tys, mx, _) =
   let
@@ -646,6 +646,8 @@
   end 
 
   val (cnstrs, dts) = split_list (map prep_dt dt_strs)
+
+  val _ = tracing ("Contructors:\n" ^ cat_lines (map @{make_string} cnstrs))
 in
   lthy
   |> Local_Theory.theory (Sign.add_consts_i (flat cnstrs))