equal
deleted
inserted
replaced
128 | ft_arg_gen cconv ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_arg_gen cconv ctxt o ft_abs ctxt (NONE, T)) ft |
128 | ft_arg_gen cconv ctxt (ft as (_, Abs (_, T, _ $ Bound 0), _)) = (ft_arg_gen cconv ctxt o ft_abs ctxt (NONE, T)) ft |
129 | ft_arg_gen _ _ (_, t, _) = raise TERM ("ft_arg", [t]) |
129 | ft_arg_gen _ _ (_, t, _) = raise TERM ("ft_arg", [t]) |
130 |
130 |
131 in |
131 in |
132 |
132 |
133 val ft_arg = ft_arg_gen arg_rewr_cconv |
133 fun ft_arg ctxt = ft_arg_gen arg_rewr_cconv ctxt |
134 val ft_imp = ft_arg_gen imp_rewr_cconv |
134 fun ft_imp ctxt = ft_arg_gen imp_rewr_cconv ctxt |
135 |
135 |
136 end |
136 end |
137 |
137 |
138 (* Move to B in !!x_1 ... x_n. B. Do not eta-expand *) |
138 (* Move to B in !!x_1 ... x_n. B. Do not eta-expand *) |
139 fun ft_params ctxt (ft as (_, t, _) : focusterm) = |
139 fun ft_params ctxt (ft as (_, t, _) : focusterm) = |