equal
deleted
inserted
replaced
1772 *} |
1772 *} |
1773 |
1773 |
1774 ML %linenosgray{*fun fail_simproc simpset redex = |
1774 ML %linenosgray{*fun fail_simproc simpset redex = |
1775 let |
1775 let |
1776 val ctxt = Simplifier.the_context simpset |
1776 val ctxt = Simplifier.the_context simpset |
1777 val _ = pwriteln (Pretty.block [Pretty.str "The redex: ", pretty_cterm ctxt redex]) |
1777 val _ = pwriteln (Pretty.block |
|
1778 [Pretty.str "The redex: ", pretty_cterm ctxt redex]) |
1778 in |
1779 in |
1779 NONE |
1780 NONE |
1780 end*} |
1781 end*} |
1781 |
1782 |
1782 text {* |
1783 text {* |
1844 *} |
1845 *} |
1845 |
1846 |
1846 ML %grayML{*fun fail_simproc' simpset redex = |
1847 ML %grayML{*fun fail_simproc' simpset redex = |
1847 let |
1848 let |
1848 val ctxt = Simplifier.the_context simpset |
1849 val ctxt = Simplifier.the_context simpset |
1849 val _ = pwriteln (Pretty.block [Pretty.str "The redex:", pretty_term ctxt redex]) |
1850 val _ = pwriteln (Pretty.block |
|
1851 [Pretty.str "The redex:", pretty_term ctxt redex]) |
1850 in |
1852 in |
1851 NONE |
1853 NONE |
1852 end*} |
1854 end*} |
1853 |
1855 |
1854 text {* |
1856 text {* |