src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 34962 807f6ce0273d
parent 34028 1e6206763036
child 34963 366a1a44aac2
equal deleted inserted replaced
34947:e1b8f2736404 34962:807f6ce0273d
  2560     val t_pred = compile_expr comp_modifiers compfuns thy
  2560     val t_pred = compile_expr comp_modifiers compfuns thy
  2561       (m, list_comb (pred, params)) inargs additional_arguments;
  2561       (m, list_comb (pred, params)) inargs additional_arguments;
  2562     val t_eval = if null outargs then t_pred else
  2562     val t_eval = if null outargs then t_pred else
  2563       let
  2563       let
  2564         val outargs_bounds = map (fn Bound i => i) outargs;
  2564         val outargs_bounds = map (fn Bound i => i) outargs;
  2565         val outargsTs = map (nth Ts) outargs_bounds;
  2565         val outargsTs = map (fn i => nth Ts (length Ts - i - 1)) outargs_bounds;
  2566         val T_pred = HOLogic.mk_tupleT outargsTs;
  2566         val T_pred = HOLogic.mk_tupleT outargsTs;
  2567         val T_compr = HOLogic.mk_ptupleT fp (rev Ts);
  2567         val T_compr = HOLogic.mk_ptupleT fp Ts;
  2568         val k = length outargs - 1;
  2568         val k = length outargs - 1;
  2569         val arrange_bounds = map_index (fn (i, j) => (k-i, k-j)) outargs_bounds
  2569         val arrange_bounds = map_index (fn (i, j) => (k-i, k-j)) outargs_bounds
  2570           |> sort (prod_ord (K EQUAL) int_ord)
  2570           |> sort (prod_ord (K EQUAL) int_ord)
  2571           |> map fst;
  2571           |> map fst;
  2572         val (outargsTs', outargsT) = split_last outargsTs;
  2572         val (outargsTs', outargsT) = split_last outargsTs;