equal
deleted
inserted
replaced
684 (if String.isPrefix lam_lifted_prefix s then Const else Free) x |
684 (if String.isPrefix lam_lifted_prefix s then Const else Free) x |
685 | constify_lifted t = t |
685 | constify_lifted t = t |
686 |
686 |
687 (* Requires bound variables not to clash with any schematic variables (as should |
687 (* Requires bound variables not to clash with any schematic variables (as should |
688 be the case right after lambda-lifting). *) |
688 be the case right after lambda-lifting). *) |
689 fun open_form (Const (@{const_name All}, _) $ Abs (_, T, t)) = |
689 fun open_form (Const (@{const_name All}, _) $ Abs (s, T, t)) = |
690 subst_bound (Var ((Name.uu ^ Int.toString (size_of_term t), 0), T), t) |
690 let |
691 |> open_form |
691 val names = Name.make_context (map fst (Term.add_var_names t [])) |
|
692 val (s, _) = Name.variant s names |
|
693 in open_form (subst_bound (Var ((s, 0), T), t)) end |
692 | open_form t = t |
694 | open_form t = t |
693 |
695 |
694 fun lift_lams_part_1 ctxt type_enc = |
696 fun lift_lams_part_1 ctxt type_enc = |
695 map close_form #> rpair ctxt |
697 map close_form #> rpair ctxt |
696 #-> Lambda_Lifting.lift_lambdas |
698 #-> Lambda_Lifting.lift_lambdas |