diff -r b4ea943ce0b7 -r f77cc54f6d47 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Thu Jan 03 12:34:26 2019 +0100
+++ b/src/Pure/pattern.ML	Thu Jan 03 14:12:44 2019 +0100
@@ -14,7 +14,6 @@
 sig
   exception Unif
   exception Pattern
-  val unify_trace_failure_raw: Config.raw
   val unify_trace_failure: bool Config.T
   val unify_types: Context.generic -> typ * typ -> Envir.env -> Envir.env
   val unify: Context.generic -> term * term -> Envir.env -> Envir.env
@@ -30,9 +29,7 @@
 exception Unif;
 exception Pattern;
 
-val unify_trace_failure_raw =
-  Config.declare ("unify_trace_failure", \<^here>) (fn _ => Config.Bool false);
-val unify_trace_failure = Config.bool unify_trace_failure_raw;
+val unify_trace_failure = Config.declare_bool ("unify_trace_failure", \<^here>) (K false);
 
 fun string_of_term ctxt env binders t =
   Syntax.string_of_term ctxt (Envir.norm_term env (subst_bounds (map Free binders, t)));