# HG changeset patch
# User blanchet
# Date 1314018165 -7200
# Node ID 99ef9fd7341b010940ab4a8c256c797bac202f78
# Parent  d3e609c87c4ce75cee2d87ddb2933aff2ef5f246
pass sound option to Sledgehammer tactic

diff -r d3e609c87c4c -r 99ef9fd7341b src/HOL/ex/sledgehammer_tactics.ML
--- a/src/HOL/ex/sledgehammer_tactics.ML	Mon Aug 22 12:17:22 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML	Mon Aug 22 15:02:45 2011 +0200
@@ -19,7 +19,7 @@
   let
     val chained_ths = [] (* a tactic has no chained ths *)
     val params as {relevance_thresholds, max_relevant, slicing, ...} =
-      ((if force_full_types then [("full_types", "true")] else [])
+      ((if force_full_types then [("sound", "true")] else [])
        @ [("timeout", string_of_int (Time.toSeconds timeout))])
        (* @ [("overlord", "true")] *)
       |> Sledgehammer_Isar.default_params ctxt