equal
deleted
inserted
replaced
211 |
211 |
212 fun obtain prop ctxt = |
212 fun obtain prop ctxt = |
213 let |
213 let |
214 val ((xs, prop'), ctxt') = Variable.focus prop ctxt; |
214 val ((xs, prop'), ctxt') = Variable.focus prop ctxt; |
215 val As = Logic.strip_imp_prems (Thm.term_of prop'); |
215 val As = Logic.strip_imp_prems (Thm.term_of prop'); |
216 in ((Binding.empty, (map (fix o Term.dest_Free o Thm.term_of) xs, As)), ctxt') end; |
216 in ((Binding.empty, (map (fix o Term.dest_Free o Thm.term_of o #2) xs, As)), ctxt') end; |
217 |
217 |
218 in |
218 in |
219 |
219 |
220 fun pretty_statement ctxt kind raw_th = |
220 fun pretty_statement ctxt kind raw_th = |
221 let |
221 let |