| changeset 329 | 5dffcab68680 |
| parent 318 | efb5fff99c96 |
| child 331 | 46100dc4a808 |
| 328:c0cae24b9d46 | 329:5dffcab68680 |
|---|---|
1653 *} |
1653 *} |
1654 |
1654 |
1655 ML{*fun fail_simproc' simpset redex = |
1655 ML{*fun fail_simproc' simpset redex = |
1656 let |
1656 let |
1657 val ctxt = Simplifier.the_context simpset |
1657 val ctxt = Simplifier.the_context simpset |
1658 val _ = tracing ("The redex: " ^ (Syntax.string_of_term ctxt redex)) |
1658 val _ = tracing ("The redex: " ^ (string_of_term ctxt redex)) |
1659 in |
1659 in |
1660 NONE |
1660 NONE |
1661 end*} |
1661 end*} |
1662 |
1662 |
1663 text {* |
1663 text {* |