equal
deleted
inserted
replaced
2405 val T = case types of [T] => T | _ => robust_const_type thy base_s0 |
2405 val T = case types of [T] => T | _ => robust_const_type thy base_s0 |
2406 val T_args = robust_const_typargs thy (base_s0, T) |
2406 val T_args = robust_const_typargs thy (base_s0, T) |
2407 val (base_name as (base_s, _), T_args) = |
2407 val (base_name as (base_s, _), T_args) = |
2408 mangle_type_args_in_const format type_enc base_name T_args |
2408 mangle_type_args_in_const format type_enc base_name T_args |
2409 val base_ary = min_ary_of sym_tab0 base_s |
2409 val base_ary = min_ary_of sym_tab0 base_s |
2410 val T_args = |
|
2411 T_args |> filter_type_args_in_const thy monom_constrs type_enc |
|
2412 base_ary base_s |
|
2413 fun do_const name = IConst (name, T, T_args) |
2410 fun do_const name = IConst (name, T, T_args) |
2414 val do_term = |
2411 val do_term = |
2415 filter_type_args_in_iterm thy monom_constrs type_enc |
2412 filter_type_args_in_iterm thy monom_constrs type_enc |
2416 #> ho_term_from_iterm ctxt format mono type_enc (SOME true) |
2413 #> ho_term_from_iterm ctxt format mono type_enc (SOME true) |
2417 val name1 as (s1, _) = |
2414 val name1 as (s1, _) = |