# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268207059 -3600
# Node ID 71bd178e478557324a3bf8b935e7a4015785684a
# Parent  5bb0149329ee2404e04a0e4b635c23f4d72892a9
alpha_bn_frees

diff -r 5bb0149329ee -r 71bd178e4785 Nominal/Fv.thy
--- a/Nominal/Fv.thy	Tue Mar 09 21:22:22 2010 +0100
+++ b/Nominal/Fv.thy	Wed Mar 10 08:44:19 2010 +0100
@@ -215,6 +215,9 @@
     "alpha_" ^ name_of_typ (nth_dtyp i)) descr);
   val alpha_types = map (fn (i, _) => nth_dtyp i --> nth_dtyp i --> @{typ bool}) descr;
   val alpha_frees = map Free (alpha_names ~~ alpha_types);
+  val alpha_bnnames = map (fn (bn, _, _) => "alpha_" ^ (Long_Name.base_name (fst (dest_Const bn)))) bns;
+  val alpha_bntypes = map (fn (_, i, _) => @{typ perm} --> nth_dtyp i --> nth_dtyp i --> @{typ bool}) bns;
+  val alpha_bnfrees = map Free (alpha_bnnames ~~ alpha_bntypes);
   fun fv_alpha_constr ith_dtyp (cname, dts) bindcs =
     let
       val Ts = map (typ_of_dtyp descr sorts) dts;