changeset 43277 | 1fd31f859fc7 |
parent 43244 | db041e88a805 |
child 43883 | aacbe67793c3 |
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Wed Jun 08 15:25:44 2011 +0200 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Wed Jun 08 15:39:55 2011 +0200 @@ -389,7 +389,7 @@ 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]