1.1 --- a/src/HOL/Tools/Function/function.ML	Sat Aug 13 21:28:01 2011 +0200
     1.2 +++ b/src/HOL/Tools/Function/function.ML	Sat Aug 13 22:04:07 2011 +0200
     1.3 @@ -125,9 +125,7 @@
     1.4            pinducts=snd pinducts', simps=NONE, inducts=NONE, termination=termination',
     1.5            fs=fs, R=R, defname=defname, is_partial=true }
     1.6  
     1.7 -        val _ =
     1.8 -          if not is_external then ()
     1.9 -          else Specification.print_consts lthy (K false) (map fst fixes)
    1.10 +        val _ = Proof_Display.print_consts is_external lthy (K false) (map fst fixes)
    1.11        in
    1.12          (info, 
    1.13           lthy |> Local_Theory.declaration false (add_function_data o morph_function_data info))