equal
deleted
inserted
replaced
57 fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x) |
57 fun prep_var (Var (ixn, _), SOME x) = SOME (ixn, x) |
58 | prep_var _ = NONE; |
58 | prep_var _ = NONE; |
59 |
59 |
60 fun prep_inst (concl, xs) = |
60 fun prep_inst (concl, xs) = |
61 let val vs = Induct.vars_of concl |
61 let val vs = Induct.vars_of concl |
62 in map_filter prep_var ((uncurry drop) (length vs - length xs, vs) ~~ xs) end; |
62 in map_filter prep_var (drop (length vs - length xs) vs ~~ xs) end; |
63 |
63 |
64 in |
64 in |
65 |
65 |
66 fun gen_induct_tac ctxt0 varss opt_rules i st = |
66 fun gen_induct_tac ctxt0 varss opt_rules i st = |
67 let |
67 let |