| changeset 59970 | e9f73d87d904 |
| parent 59647 | c6f413b660cf |
| child 60171 | b3be7677461e |
--- a/src/HOL/Tools/simpdata.ML Wed Apr 08 16:24:22 2015 +0200 +++ b/src/HOL/Tools/simpdata.ML Wed Apr 08 19:39:08 2015 +0200 @@ -147,7 +147,7 @@ structure Splitter = Splitter ( - val thy = @{theory} + val context = @{context} val mk_eq = mk_eq val meta_eq_to_iff = @{thm meta_eq_to_obj_eq} val iffD = @{thm iffD2}