--- a/src/HOL/Mutabelle/mutabelle_extra.ML Fri Mar 06 14:01:08 2015 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML Fri Mar 06 15:58:56 2015 +0100
@@ -401,7 +401,7 @@
|> map Mutabelle.freeze |> map freezeT
(* |> filter (not o is_forbidden_mutant) *)
|> map_filter (try (Sign.cert_term thy))
- |> filter (is_some o try (Thm.cterm_of thy))
+ |> filter (is_some o try (Thm.global_cterm_of thy))
|> filter (is_some o try (Syntax.check_term (Proof_Context.init_global thy)))
|> take_random max_mutants
val _ = map (fn t => writeln ("MUTANT: " ^ Syntax.string_of_term_global thy t)) mutants