equal
deleted
inserted
replaced
448 do_term extra_us (SOME (typ_from_atp tfrees typ_u)) term_u |
448 do_term extra_us (SOME (typ_from_atp tfrees typ_u)) term_u |
449 | _ => raise FO_TERM us |
449 | _ => raise FO_TERM us |
450 else if s' = predicator_name then |
450 else if s' = predicator_name then |
451 do_term [] (SOME @{typ bool}) (hd us) |
451 do_term [] (SOME @{typ bool}) (hd us) |
452 else if s' = app_op_name then |
452 else if s' = app_op_name then |
453 do_term (nth us 1 :: extra_us) opt_T (hd us) |
453 do_term (List.last us :: extra_us) opt_T (nth us (length us - 2)) |
454 else if s' = type_pred_name then |
454 else if s' = type_pred_name then |
455 @{const True} (* ignore type predicates *) |
455 @{const True} (* ignore type predicates *) |
456 else |
456 else |
457 let |
457 let |
458 val num_ty_args = |
458 val num_ty_args = |