diff -r 7bc38b93a1fc -r 9ae285ce814e Nominal/nominal_function.ML
--- a/Nominal/nominal_function.ML	Sun Apr 06 13:07:24 2014 +0100
+++ b/Nominal/nominal_function.ML	Fri May 16 08:38:23 2014 +0100
@@ -181,7 +181,8 @@
           pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
           fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts}
 
-        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}