--- a/Nominal/NewAlpha.thy	Mon May 10 12:04:40 2010 +0200
+++ b/Nominal/NewAlpha.thy	Mon May 10 15:09:32 2010 +0200
@@ -73,7 +73,7 @@
     else Const (@{const_name supp},
       Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ "atom set"})
   val fvs = map fv_for_dt body_dts;
-  val fv = mk_compound_fv fvs;
+  val fv = mk_compound_fv' lthy fvs;
   fun alpha_for_dt dt =
     if Datatype_Aux.is_rec_type dt
     then nth alpha_frees (Datatype_Aux.body_index dt)
@@ -81,7 +81,7 @@
       Datatype_Aux.typ_of_dtyp dt_descr sorts dt -->
       Datatype_Aux.typ_of_dtyp dt_descr sorts dt --> @{typ bool})
   val alphas = map alpha_for_dt body_dts;
-  val alpha = mk_compound_alpha alphas;
+  val alpha = mk_compound_alpha' lthy alphas;
   val alpha_gen_pre = Const (alpha_const, dummyT) $ lhs $ alpha $ fv $ (Bound 0) $ rhs
   val alpha_gen_ex = HOLogic.exists_const @{typ perm} $ Abs ("p", @{typ perm}, alpha_gen_pre)
   val t = Syntax.check_term lthy alpha_gen_ex