diff -r 9ecf2cbfc80d -r 11a4001b06c6 src/HOL/Tools/Function/function.ML
--- a/src/HOL/Tools/Function/function.ML	Fri May 09 21:03:44 2014 +0200
+++ b/src/HOL/Tools/Function/function.ML	Fri May 09 22:04:50 2014 +0200
@@ -132,7 +132,9 @@
           fs=fs, R=R, dom=dom, defname=defname, is_partial=true, cases=flat cases',
           pelims=pelims',elims=NONE}
 
-        val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
+        val _ =
+          Proof_Display.print_consts do_print (Position.thread_data ()) lthy
+            (K false) (map fst fixes)
       in
         (info,
          lthy |> Local_Theory.declaration {syntax = false, pervasive = false}