equal
deleted
inserted
replaced
93 val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs; |
93 val atomized_defs = map (map (Conv.fconv_rule Induct.atomize_cterm)) defs; |
94 |
94 |
95 val finish_rule = |
95 val finish_rule = |
96 split_all_tuples |
96 split_all_tuples |
97 #> rename_params_rule true |
97 #> rename_params_rule true |
98 (map (Name.clean o ProofContext.revert_skolem defs_ctxt o fst) avoiding); |
98 (map (Name.clean o Variable.revert_fixed defs_ctxt o fst) avoiding); |
99 |
99 |
100 fun rule_cases ctxt r = |
100 fun rule_cases ctxt r = |
101 let val r' = if simp then Induct.simplified_rule ctxt r else r |
101 let val r' = if simp then Induct.simplified_rule ctxt r else r |
102 in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end; |
102 in Rule_Cases.make_nested (Thm.prop_of r') (Induct.rulified_term r') end; |
103 in |
103 in |