# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1273496972 -7200
# Node ID c861b53d0cde70a082ec679ef09a450cd8f280ad
# Parent  78ffb5b00e4fd42d25694a18e441c22f0e93eff9
Use mk_compound_fv' and mk_compound_rel'

diff -r 78ffb5b00e4f -r c861b53d0cde Nominal/NewAlpha.thy
--- 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