--- a/Nominal/NewParser.thy	Mon May 03 09:55:43 2010 +0200
+++ b/Nominal/NewParser.thy	Mon May 03 09:57:05 2010 +0200
@@ -335,7 +335,7 @@
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names);
   val {descr, sorts, ...} = dtinfo;
   val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr;
-  val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr)
+  val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr)
 
   val all_full_tnames = map (fn (_, (n, _, _)) => n) descr;
   val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy1)) all_full_tnames;
@@ -403,8 +403,8 @@
   val raw_consts =
     flat (map (fn (i, (_, _, l)) =>
       map (fn (cname, dts) =>
-        Const (cname, map (typ_of_dtyp descr sorts) dts --->
-          typ_of_dtyp descr sorts (DtRec i))) l) descr);
+        Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts --->
+          Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr);
   val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7;
   val _ = warning "Proving respects";
   val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;