src/Tools/induct.ML
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 *)