--- 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