| changeset 64556 | 851ae0e7b09c |
| parent 63718 | 600cf5c8f2ba |
| child 69575 | f77cc54f6d47 |
--- a/src/Pure/pattern.ML Mon Dec 12 17:40:06 2016 +0100 +++ b/src/Pure/pattern.ML Tue Dec 13 11:51:42 2016 +0100 @@ -31,7 +31,7 @@ exception Pattern; val unify_trace_failure_raw = - Config.declare ("unify_trace_failure", @{here}) (fn _ => Config.Bool false); + Config.declare ("unify_trace_failure", \<^here>) (fn _ => Config.Bool false); val unify_trace_failure = Config.bool unify_trace_failure_raw; fun string_of_term ctxt env binders t =