equal
deleted
inserted
replaced
90 val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list; |
90 val ((insts, defs), defs_ctxt) = fold_map Induct.add_defs def_insts ctxt |>> split_list; |
91 val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs; |
91 val atomized_defs = map (map (Conv.fconv_rule ObjectLogic.atomize)) defs; |
92 |
92 |
93 val finish_rule = |
93 val finish_rule = |
94 split_all_tuples |
94 split_all_tuples |
95 #> rename_params_rule true (map (ProofContext.revert_skolem defs_ctxt o fst) avoiding); |
95 #> rename_params_rule true |
|
96 (map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding); |
96 fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (Induct.rulified_term r); |
97 fun rule_cases r = RuleCases.make_nested true (Thm.prop_of r) (Induct.rulified_term r); |
97 in |
98 in |
98 (fn i => fn st => |
99 (fn i => fn st => |
99 rules |
100 rules |
100 |> inst_mutual_rule ctxt insts avoiding |
101 |> inst_mutual_rule ctxt insts avoiding |