# HG changeset patch # User Christian Urban # Date 1272430507 -7200 # Node ID 700024ec18da016286d1884b9dc90677c07c634d # Parent b6b3374a402d61db6a826a018fc167fa8e216df6 tuned diff -r b6b3374a402d -r 700024ec18da Nominal/NewFv.thy --- a/Nominal/NewFv.thy Wed Apr 28 06:40:10 2010 +0200 +++ b/Nominal/NewFv.thy Wed Apr 28 06:55:07 2010 +0200 @@ -153,7 +153,7 @@ *} ML {* -fun fv_bns thy dt_info fv_frees bns bmlll = +fun fv_bns thy dt_info fv_frees bn_funs bclauses = let fun mk_fvbn_free (bn, ith, _) = let @@ -161,12 +161,12 @@ in (fvbn_name, Free (fvbn_name, fastype_of (nth fv_frees ith))) end; - val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bns); - val bn_fvbn = (map (fn (bn, _, _) => bn) bns) ~~ fvbn_frees - val bmlls = map (fn (_, i, _) => nth bmlll i) bns; - val eqs = map2 (fv_bn thy dt_info fv_frees bn_fvbn) bmlls (fvbn_frees ~~ bns); + val (fvbn_names, fvbn_frees) = split_list (map mk_fvbn_free bn_funs); + val bn_fvbn = (map (fn (bn, _, _) => bn) bn_funs) ~~ fvbn_frees + val bmlls = map (fn (_, i, _) => nth bclauses i) bn_funs; + val eqs = map2 (fv_bn thy dt_info fv_frees bn_fvbn) bmlls (fvbn_frees ~~ bn_funs); in - (bn_fvbn, (fvbn_names, eqs)) + (bn_fvbn, fvbn_names, eqs) end *} @@ -220,21 +220,22 @@ *} ML {* -fun define_raw_fv dt_info bns bmlll lthy = +fun define_raw_fv dt_info bn_funs bclauses lthy = let val thy = ProofContext.theory_of lthy; - val {descr, sorts, ...} = dt_info; - - val fv_names = prefix_dt_names descr sorts "fv_" + val {descr as dt_descr, sorts, ...} = dt_info; - val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) descr; + val fv_names = prefix_dt_names dt_descr sorts "fv_" + val fv_types = map (fn (i, _) => nth_dtyp descr sorts i --> @{typ "atom set"}) dt_descr; val fv_frees = map Free (fv_names ~~ fv_types); - val (bn_fvbn, (fv_bn_names, fv_bn_eqs)) = fv_bns thy dt_info fv_frees bns bmlll; + + val (bn_fvbn, fv_bn_names, fv_bn_eqs) = + fv_bns thy dt_info fv_frees bn_funs bclauses; val fvbns = map snd bn_fvbn; val fv_nums = 0 upto (length fv_frees - 1) - val fv_eqs = map2 (fv thy dt_info fv_frees bn_fvbn) bmlll (fv_frees ~~ fv_nums); + val fv_eqs = map2 (fv thy dt_info fv_frees bn_fvbn) bclauses (fv_frees ~~ fv_nums); val fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names) val fv_eqs_binds = map (fn x => (Attrib.empty_binding, x)) (flat fv_eqs @ flat fv_bn_eqs)