diff -r b14bd153a753 -r 7f6b2634d853 src/Pure/type_infer_context.ML
--- a/src/Pure/type_infer_context.ML	Sun Apr 06 15:51:02 2014 +0200
+++ b/src/Pure/type_infer_context.ML	Sun Apr 06 16:36:28 2014 +0200
@@ -20,7 +20,8 @@
 
 (* constraints *)
 
-val const_sorts = Config.bool (Config.declare "const_sorts" (K (Config.Bool true)));
+val const_sorts =
+  Config.bool (Config.declare ("const_sorts", @{here}) (K (Config.Bool true)));
 
 fun const_type ctxt =
   try ((not (Config.get ctxt const_sorts) ? Type.strip_sorts) o