--- a/Nominal/nominal_function.ML	Mon Aug 15 10:43:22 2011 +0200
+++ b/Nominal/nominal_function.ML	Mon Aug 15 17:42:35 2011 +0200
@@ -181,9 +181,7 @@
           pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
           fs=fs, R=R, defname=defname, is_partial=true, eqvts=eqvts}
 
-        val _ =
-          if not is_external then ()
-          else Specification.print_consts lthy (K false) (map fst fixes)
+        val _ = Proof_Display.print_consts is_external lthy (K false) (map fst fixes)
       in
         (info, 
          lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))