changeset 62913 | 13252110a6fe |
parent 61853 | fb7756087101 |
child 62958 | b41c1cb5e251 |
--- a/src/Tools/induct.ML Thu Apr 07 22:09:23 2016 +0200 +++ b/src/Tools/induct.ML Fri Apr 08 20:15:20 2016 +0200 @@ -173,8 +173,7 @@ val rearrange_eqs_simproc = Simplifier.make_simproc @{context} "rearrange_eqs" {lhss = [@{term "Pure.all(t)"}], - proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct, - identifier = []}; + proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct}; (* rotate k premises to the left by j, skipping over first j premises *)