src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML

--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun May 12 20:30:34 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Sun May 12 20:46:17 2013 +0200
@@ -733,7 +733,7 @@
           val metis_ft = AList.defined (op =) args metis_ftK
           val trivial =
             if AList.lookup (op =) args check_trivialK |> the_default trivial_default
-                            |> Bool.fromString |> the then
+                            |> Markup.parse_bool then
               Try0.try0 (SOME try_timeout) ([], [], [], []) pre
               handle TimeLimit.TimeOut => false
             else false