diff -r 621ebd8b13c4 -r 715ab84065a0 Nominal/NewParser.thy
--- 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))