387 val lhs_arg = foldr1 HOLogic.mk_prod bound_args |
387 val lhs_arg = foldr1 HOLogic.mk_prod bound_args |
388 val lhs = mk_pair (lhs_binds, lhs_arg); |
388 val lhs = mk_pair (lhs_binds, lhs_arg); |
389 val rhs_binds = fv_binds args2 rbinds; |
389 val rhs_binds = fv_binds args2 rbinds; |
390 val rhs_arg = foldr1 HOLogic.mk_prod bound_args2; |
390 val rhs_arg = foldr1 HOLogic.mk_prod bound_args2; |
391 val rhs = mk_pair (rhs_binds, rhs_arg); |
391 val rhs = mk_pair (rhs_binds, rhs_arg); |
392 val _ = tracing (PolyML.makestring bound_in_ty_nos); |
|
393 val fvs = map (nth fv_frees) ((body_index dt) :: bound_in_ty_nos); |
392 val fvs = map (nth fv_frees) ((body_index dt) :: bound_in_ty_nos); |
394 val _ = tracing (PolyML.makestring fvs); |
|
395 val fv = mk_compound_fv fvs; |
393 val fv = mk_compound_fv fvs; |
396 val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos); |
394 val alphas = map (nth alpha_frees) ((body_index dt) :: bound_in_ty_nos); |
397 val _ = tracing (PolyML.makestring alphas); |
|
398 val alpha = mk_compound_alpha alphas; |
395 val alpha = mk_compound_alpha alphas; |
399 val pi = foldr1 add_perm (distinct (op =) rpis); |
396 val pi = foldr1 add_perm (distinct (op =) rpis); |
400 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
397 val alpha_gen_pre = Const (@{const_name alpha_gen}, dummyT) $ lhs $ alpha $ fv $ pi $ rhs; |
401 val _ = tracing (PolyML.makestring alpha_gen_pre); |
|
402 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
398 val alpha_gen = Syntax.check_term lthy alpha_gen_pre |
403 in |
399 in |
404 alpha_gen |
400 alpha_gen |
405 end |
401 end |
406 else |
402 else |
447 val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) |
443 val (fv_names_snd, fv_eqs_snd) = apsnd flat (split_list (map fst (filter filter_fun all_fvs))) |
448 val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); |
444 val fv_eqs_all = fv_eqs_fst @ (flat fv_bn_eqs); |
449 val fv_names_all = fv_names_fst @ fv_bn_names; |
445 val fv_names_all = fv_names_fst @ fv_bn_names; |
450 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
446 val add_binds = map (fn x => (Attrib.empty_binding, x)) |
451 (* Function_Fun.add_fun Function_Common.default_config ... true *) |
447 (* Function_Fun.add_fun Function_Common.default_config ... true *) |
452 (* val _ = map tracing (map (Syntax.string_of_term @{context}) fv_eqs_all)*) |
|
453 val (fvs, lthy') = (Primrec.add_primrec |
448 val (fvs, lthy') = (Primrec.add_primrec |
454 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) |
449 (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names_all) (add_binds fv_eqs_all) lthy) |
455 val (fvs2, lthy'') = |
450 val (fvs2, lthy'') = |
456 if fv_eqs_snd = [] then (([], []), lthy') else |
451 if fv_eqs_snd = [] then (([], []), lthy') else |
457 (Primrec.add_primrec |
452 (Primrec.add_primrec |