468 end |
468 end |
469 else if s' = type_pred_name then |
469 else if s' = type_pred_name then |
470 @{const True} (* ignore type predicates *) |
470 @{const True} (* ignore type predicates *) |
471 else |
471 else |
472 let |
472 let |
|
473 val new_skolem = String.isPrefix new_skolem_const_prefix s |
473 val num_ty_args = |
474 val num_ty_args = |
474 length us - the_default 0 (Symtab.lookup sym_tab s) |
475 length us - the_default 0 (Symtab.lookup sym_tab s) |
475 val (type_us, term_us) = |
476 val (type_us, term_us) = |
476 chop num_ty_args us |>> append mangled_us |
477 chop num_ty_args us |>> append mangled_us |
477 val term_ts = map (do_term [] NONE) term_us |
478 val term_ts = map (do_term [] NONE) term_us |
478 val T = |
479 val T = |
479 (if not (null type_us) andalso |
480 (if not (null type_us) andalso |
480 num_type_args thy s' = length type_us then |
481 num_type_args thy s' = length type_us then |
481 try (Sign.const_instance thy) |
482 let val Ts = type_us |> map (typ_from_atp ctxt) in |
482 (s', map (typ_from_atp ctxt) type_us) |
483 if new_skolem then |
|
484 SOME (Type_Infer.paramify_vars (tl Ts ---> hd Ts)) |
|
485 else |
|
486 try (Sign.const_instance thy) (s', Ts) |
|
487 end |
483 else |
488 else |
484 NONE) |
489 NONE) |
485 |> (fn SOME T => T |
490 |> (fn SOME T => T |
486 | NONE => map slack_fastype_of term_ts ---> |
491 | NONE => map slack_fastype_of term_ts ---> |
487 (case opt_T of |
492 (case opt_T of |
488 SOME T => T |
493 SOME T => T |
489 | NONE => HOLogic.typeT)) |
494 | NONE => HOLogic.typeT)) |
490 val s' = s' |> unproxify_const |
495 val t = |
491 in list_comb (Const (s', T), term_ts @ extra_ts) end |
496 if new_skolem then |
|
497 Var ((new_skolem_var_name_from_const s, var_index), T) |
|
498 else |
|
499 Const (unproxify_const s', T) |
|
500 in list_comb (t, term_ts @ extra_ts) end |
492 end |
501 end |
493 | NONE => (* a free or schematic variable *) |
502 | NONE => (* a free or schematic variable *) |
494 let |
503 let |
495 val ts = map (do_term [] NONE) us @ extra_ts |
504 val ts = map (do_term [] NONE) us @ extra_ts |
496 val T = map slack_fastype_of ts ---> HOLogic.typeT |
505 val T = map slack_fastype_of ts ---> HOLogic.typeT |