419 fun mk_ind_concl ((c, P), (ts, x)) = |
419 fun mk_ind_concl ((c, P), (ts, x)) = |
420 let val T = HOLogic.dest_setT (fastype_of c); |
420 let val T = HOLogic.dest_setT (fastype_of c); |
421 val ps = if_none (assoc (factors, P)) []; |
421 val ps = if_none (assoc (factors, P)) []; |
422 val Ts = prodT_factors [] ps T; |
422 val Ts = prodT_factors [] ps T; |
423 val (frees, x') = foldr (fn (T', (fs, s)) => |
423 val (frees, x') = foldr (fn (T', (fs, s)) => |
424 ((Free (s, T'))::fs, bump_string s)) (Ts, ([], x)); |
424 ((Free (s, T'))::fs, Symbol.bump_string s)) (Ts, ([], x)); |
425 val tuple = mk_tuple [] ps T frees; |
425 val tuple = mk_tuple [] ps T frees; |
426 in ((HOLogic.mk_binop "op -->" |
426 in ((HOLogic.mk_binop "op -->" |
427 (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x') |
427 (HOLogic.mk_mem (tuple, c), P $ tuple))::ts, x') |
428 end; |
428 end; |
429 |
429 |