| changeset 60774 | 6c28d8ed2488 |
| parent 60644 | 4af8b9c2b52f |
| child 69593 | 3dda49e08b9d |
--- a/src/FOLP/simpdata.ML Thu Jul 23 22:13:42 2015 +0200 +++ b/src/FOLP/simpdata.ML Fri Jul 24 22:16:39 2015 +0200 @@ -76,7 +76,7 @@ open FOLP_Simp; -val auto_ss = empty_ss setauto ares_tac [@{thm TrueI}]; +val auto_ss = empty_ss setauto (fn ctxt => ares_tac ctxt @{thms TrueI}); val IFOLP_ss = auto_ss addcongs FOLP_congs |> fold (addrew @{context}) IFOLP_rews;