src/HOL/Tools/Function/function.ML

         val info = { add_simps=addsmps, fnames=fnames, case_names=cnames, psimps=psimps',
           pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
           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}
           (add_function_data o transform_function_data info))
       end