diff -r 3365fce80f0f -r 6eacf60ce41d Nominal/Fv.thy
--- a/Nominal/Fv.thy	Fri Feb 26 10:34:04 2010 +0100
+++ b/Nominal/Fv.thy	Fri Feb 26 13:57:43 2010 +0100
@@ -92,12 +92,10 @@
 
 (* TODO: Notice datatypes without bindings and replace alpha with equality *)
 ML {*
-(* Currently needs just one full_tname to access Datatype *)
-fun define_fv_alpha full_tname bindsall lthy =
+fun define_fv_alpha (dt_info : Datatype_Aux.info) bindsall lthy =
 let
   val thy = ProofContext.theory_of lthy;
-  val {descr, ...} = Datatype.the_info thy full_tname;
-  val sorts = []; (* TODO *)
+  val {descr, sorts, ...} = dt_info;
   fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i);
   val fv_names = Datatype_Prop.indexify_names (map (fn (i, _) =>
     "fv_" ^ name_of_typ (nth_dtyp i)) descr);