equal
deleted
inserted
replaced
150 | Abs (_, T, _ $ Bound 0) => abs_pconv (arg_pconv_gen cv0 cv) (NONE, T) ctxt tytenv ct |
150 | Abs (_, T, _ $ Bound 0) => abs_pconv (arg_pconv_gen cv0 cv) (NONE, T) ctxt tytenv ct |
151 | t => raise TERM ("arg_pconv_gen", [t]) |
151 | t => raise TERM ("arg_pconv_gen", [t]) |
152 |
152 |
153 in |
153 in |
154 |
154 |
155 val arg_pconv = arg_pconv_gen CConv.arg_cconv |
155 fun arg_pconv ctxt = arg_pconv_gen CConv.arg_cconv ctxt |
156 val imp_pconv = arg_pconv_gen (CConv.concl_cconv 1) |
156 fun imp_pconv ctxt = arg_pconv_gen (CConv.concl_cconv 1) ctxt |
157 |
157 |
158 end |
158 end |
159 |
159 |
160 (* Move to B in !!x_1 ... x_n. B. Do not eta-expand *) |
160 (* Move to B in !!x_1 ... x_n. B. Do not eta-expand *) |
161 fun params_pconv cv ctxt tytenv ct = |
161 fun params_pconv cv ctxt tytenv ct = |