281 val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t |
281 val split = case t_compr of (Const (@{const_name Collect}, _) $ t) => t |
282 | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr); |
282 | _ => error ("Not a set comprehension: " ^ Syntax.string_of_term ctxt t_compr); |
283 val (body, Ts, fp) = HOLogic.strip_psplits split; |
283 val (body, Ts, fp) = HOLogic.strip_psplits split; |
284 val output_names = Name.variant_list (Term.add_free_names body []) |
284 val output_names = Name.variant_list (Term.add_free_names body []) |
285 (map (fn i => "x" ^ string_of_int i) (1 upto length Ts)) |
285 (map (fn i => "x" ^ string_of_int i) (1 upto length Ts)) |
286 val output_frees = map2 (curry Free) output_names (rev Ts) |
286 val output_frees = rev (map2 (curry Free) output_names Ts) |
287 val body = subst_bounds (output_frees, body) |
287 val body = subst_bounds (output_frees, body) |
288 val (pred as Const (name, T), all_args) = |
288 val (pred as Const (name, T), all_args) = |
289 case strip_comb body of |
289 case strip_comb body of |
290 (Const (name, T), all_args) => (Const (name, T), all_args) |
290 (Const (name, T), all_args) => (Const (name, T), all_args) |
291 | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head) |
291 | (head, _) => error ("Not a constant: " ^ Syntax.string_of_term ctxt head) |