src/HOL/Mutabelle/mutabelle_extra.ML

 
 (* (theory -> thm -> bool -> term list -> mtd list -> 'a) -> theory -> mtd list -> thm -> 'a *)
 fun mutate_theorem create_entry thy mtds thm =
   let
     val exec = is_executable_thm thy thm
-    val _ = Output.tracing (if exec then "EXEC" else "NOEXEC")
+    val _ = tracing (if exec then "EXEC" else "NOEXEC")
     val mutants =
           (if num_mutations = 0 then
              [Thm.prop_of thm]
            else
              Mutabelle.mutate_mix (Thm.prop_of thm) thy comms forbidden