| changeset 62958 | b41c1cb5e251 |
| parent 62913 | 13252110a6fe |
| child 63344 | c9910404cc8a |
--- a/src/Tools/induct.ML Tue Apr 12 13:49:37 2016 +0200 +++ b/src/Tools/induct.ML Tue Apr 12 14:38:57 2016 +0200 @@ -172,7 +172,7 @@ val rearrange_eqs_simproc = Simplifier.make_simproc @{context} "rearrange_eqs" - {lhss = [@{term "Pure.all(t)"}], + {lhss = [@{term "Pure.all (t :: 'a::{} \<Rightarrow> prop)"}], proc = fn _ => fn ctxt => fn ct => mk_swap_rrule ctxt ct};