equal
deleted
inserted
replaced
691 | open_form t = t |
691 | open_form t = t |
692 |
692 |
693 fun lift_lams_part_1 ctxt type_enc = |
693 fun lift_lams_part_1 ctxt type_enc = |
694 map (Envir.eta_contract #> close_form) #> rpair ctxt |
694 map (Envir.eta_contract #> close_form) #> rpair ctxt |
695 #-> Lambda_Lifting.lift_lambdas |
695 #-> Lambda_Lifting.lift_lambdas |
696 (SOME (if polymorphism_of_type_enc type_enc = Polymorphic then |
696 (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then |
697 lam_lifted_poly_prefix |
697 lam_lifted_poly_prefix |
698 else |
698 else |
699 lam_lifted_mono_prefix)) |
699 lam_lifted_mono_prefix) ^ "_a")) |
700 Lambda_Lifting.is_quantifier |
700 Lambda_Lifting.is_quantifier |
701 #> fst |
701 #> fst |
702 val lift_lams_part_2 = pairself (map (open_form o constify_lifted)) |
702 val lift_lams_part_2 = pairself (map (open_form o constify_lifted)) |
703 val lift_lams = lift_lams_part_2 ooo lift_lams_part_1 |
703 val lift_lams = lift_lams_part_2 ooo lift_lams_part_1 |
704 |
704 |