--- a/Nominal/Parser.thy	Mon May 03 10:15:23 2010 +0200
+++ b/Nominal/Parser.thy	Mon May 03 11:35:38 2010 +0200
@@ -1,8 +1,8 @@
 theory Parser
-imports "../Nominal-General/Nominal2_Atoms" 
-        "../Nominal-General/Nominal2_Eqvt" 
-        "../Nominal-General/Nominal2_Supp" 
-        "Perm" "Equivp" "Rsp" "Lift"
+imports "../Nominal-General/Nominal2_Atoms"
+        "../Nominal-General/Nominal2_Eqvt"
+        "../Nominal-General/Nominal2_Supp"
+        "Perm" "Equivp" "Rsp" "Lift" "Fv"
 begin
 
 section{* Interface for nominal_datatype *}
@@ -372,9 +372,9 @@
 
   val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names);
   val {descr, sorts, ...} = dtinfo;
-  fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
+  fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i);
   val raw_tys = map (fn (i, _) => nth_dtyp 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 lthy2)) all_full_tnames;
   val rel_dtinfos = List.take (dtinfos, (length dts));
@@ -423,8 +423,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 _ = tracing "Proving respects";
   val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;