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