equal
deleted
inserted
replaced
538 trans) |
538 trans) |
539 |> (fn trans => |
539 |> (fn trans => |
540 if trans = concealedN then |
540 if trans = concealedN then |
541 rpair [] o map (conceal_lambdas ctxt) |
541 rpair [] o map (conceal_lambdas ctxt) |
542 else if trans = liftingN then |
542 else if trans = liftingN then |
543 map (close_form o Envir.eta_contract) |
543 map (close_form o Envir.eta_contract) #> rpair ctxt |
544 #> Lambda_Lifting.lift_lambdas ctxt false #> snd #> swap |
544 #-> Lambda_Lifting.lift_lambdas NONE Lambda_Lifting.is_quantifier |
|
545 #> fst |
545 else if trans = combinatorsN then |
546 else if trans = combinatorsN then |
546 rpair [] o map (introduce_combinators ctxt) |
547 rpair [] o map (introduce_combinators ctxt) |
547 else if trans = lambdasN then |
548 else if trans = lambdasN then |
548 rpair [] o map (Envir.eta_contract) |
549 rpair [] o map (Envir.eta_contract) |
549 else |
550 else |