equal
deleted
inserted
replaced
102 val prems' = prems |
102 val prems' = prems |
103 |> map (incr_boundvars 1) |
103 |> map (incr_boundvars 1) |
104 |> map (add_c_prop true Ps (Bound 0, c_name, c_ty)) |
104 |> map (add_c_prop true Ps (Bound 0, c_name, c_ty)) |
105 |
105 |
106 val avoid_trm' = avoid_trm |
106 val avoid_trm' = avoid_trm |
107 |> (curry list_abs_free) (params @ [(c_name, c_ty)]) |
107 |> fold_rev absfree (params @ [(c_name, c_ty)]) |
108 |> strip_abs_body |
108 |> strip_abs_body |
109 |> (fn t => mk_fresh_star_ty c_ty t (Bound 0)) |
109 |> (fn t => mk_fresh_star_ty c_ty t (Bound 0)) |
110 |> HOLogic.mk_Trueprop |
110 |> HOLogic.mk_Trueprop |
111 |
111 |
112 val prems'' = |
112 val prems'' = |