equal
deleted
inserted
replaced
85 val add_post = map_post o MetaSimplifier.add_simp; |
85 val add_post = map_post o MetaSimplifier.add_simp; |
86 val del_post = map_post o MetaSimplifier.del_simp; |
86 val del_post = map_post o MetaSimplifier.del_simp; |
87 |
87 |
88 fun add_unfold_post raw_thm thy = |
88 fun add_unfold_post raw_thm thy = |
89 let |
89 let |
90 val thm = Local_Defs.meta_rewrite_rule (ProofContext.init thy) raw_thm; |
90 val thm = Local_Defs.meta_rewrite_rule (ProofContext.init_global thy) raw_thm; |
91 val thm_sym = Thm.symmetric thm; |
91 val thm_sym = Thm.symmetric thm; |
92 in |
92 in |
93 thy |> map_pre_post (fn (pre, post) => |
93 thy |> map_pre_post (fn (pre, post) => |
94 (pre |> MetaSimplifier.add_simp thm, post |> MetaSimplifier.del_simp thm_sym)) |
94 (pre |> MetaSimplifier.add_simp thm, post |> MetaSimplifier.del_simp thm_sym)) |
95 end; |
95 end; |
155 |
155 |
156 fun postprocess_term thy = term_of_conv thy (postprocess_conv thy); |
156 fun postprocess_term thy = term_of_conv thy (postprocess_conv thy); |
157 |
157 |
158 fun print_codeproc thy = |
158 fun print_codeproc thy = |
159 let |
159 let |
160 val ctxt = ProofContext.init thy; |
160 val ctxt = ProofContext.init_global thy; |
161 val pre = (#pre o the_thmproc) thy; |
161 val pre = (#pre o the_thmproc) thy; |
162 val post = (#post o the_thmproc) thy; |
162 val post = (#post o the_thmproc) thy; |
163 val functrans = (map fst o #functrans o the_thmproc) thy; |
163 val functrans = (map fst o #functrans o the_thmproc) thy; |
164 in |
164 in |
165 (Pretty.writeln o Pretty.chunks) [ |
165 (Pretty.writeln o Pretty.chunks) [ |