src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML

           [] => error ("No specification for " ^ (Syntax.string_of_term_global thy t))
         | ((_, (_, ths)) :: _) => filter_defs ths)
     | ths => rev ths
     val _ =
       if show_intermediate_results options then
-        Output.tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
+        tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
           commas (map (Display.string_of_thm_global thy) spec))
       else ()
   in
     spec
   end