Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Use mk_compound_fv' and mk_compound_rel'
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 10 May 2010 15:09:32 +0200
changeset 2087 c861b53d0cde
parent 2085 78ffb5b00e4f
child 2088 248bb900727e
child 2089 e9f089a5cc17
Use mk_compound_fv' and mk_compound_rel'
Nominal/NewAlpha.thy file | annotate | diff | comparison | revisions 
--- 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
nominal2