# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273496993 -7200
# Node ID 248bb900727ea3c308c1ef300d8d6503f6c748ed
# Parent  fd305c609c6cd0c2b3d1819a8c9a2d438e1c5939# Parent  c861b53d0cde70a082ec679ef09a450cd8f280ad
merge

diff -r fd305c609c6c -r 248bb900727e Nominal/NewAlpha.thy
--- a/Nominal/NewAlpha.thy	Mon May 10 12:05:13 2010 +0200
+++ b/Nominal/NewAlpha.thy	Mon May 10 15:09:53 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