# HG changeset patch
# User sultana
# Date 1333062090 -3600
# Node ID 06e6f352df1bff3fddc90edfa1b9a88d0e674edb
# Parent  fbcb7024fc938468d5b7f65a09b152646dd3c7d6
made Mirabelle-SH's 'trivial' check optional;

diff -r fbcb7024fc93 -r 06e6f352df1b src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Mar 29 22:52:24 2012 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Fri Mar 30 00:01:30 2012 +0100
@@ -26,6 +26,7 @@
 val sh_minimizeK = "sh_minimize" (*refers to minimizer run within Sledgehammer*)
 val max_new_mono_instancesK = "max_new_mono_instances"
 val max_mono_itersK = "max_mono_iters"
+val check_trivialK = "check_trivial" (*false by default*)
 
 fun sh_tag id = "#" ^ string_of_int id ^ " sledgehammer: "
 fun minimize_tag id = "#" ^ string_of_int id ^ " minimize (sledgehammer): "
@@ -701,8 +702,11 @@
           val minimize = AList.defined (op =) args minimizeK
           val metis_ft = AList.defined (op =) args metis_ftK
           val trivial =
-            Try0.try0 (SOME try_timeout) ([], [], [], []) pre
-            handle TimeLimit.TimeOut => false
+            if AList.lookup (op =) args check_trivialK |> the_default "false"
+                            |> Bool.fromString |> the then
+              Try0.try0 (SOME try_timeout) ([], [], [], []) pre
+              handle TimeLimit.TimeOut => false
+            else false
           fun apply_reconstructor m1 m2 =
             if metis_ft
             then