equal
deleted
inserted
replaced
179 val thy = Proof_Context.theory_of ctxt; |
179 val thy = Proof_Context.theory_of ctxt; |
180 val pre = (#pre o the_thmproc) thy; |
180 val pre = (#pre o the_thmproc) thy; |
181 val post = (#post o the_thmproc) thy; |
181 val post = (#post o the_thmproc) thy; |
182 val functrans = (map fst o #functrans o the_thmproc) thy; |
182 val functrans = (map fst o #functrans o the_thmproc) thy; |
183 in |
183 in |
184 (Pretty.writeln o Pretty.chunks) [ |
184 Pretty.writeln_chunks [ |
185 Pretty.block [ |
185 Pretty.block [ |
186 Pretty.str "preprocessing simpset:", |
186 Pretty.str "preprocessing simpset:", |
187 Pretty.fbrk, |
187 Pretty.fbrk, |
188 Simplifier.pretty_simpset (put_simpset pre ctxt) |
188 Simplifier.pretty_simpset (put_simpset pre ctxt) |
189 ], |
189 ], |