src/HOL/ex/sledgehammer_tactics.ML
changeset 42642 f5b4b9d4acda
parent 42638 a7a30721767a
child 42944 9e620869a576
     1.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Mon May 02 22:52:15 2011 +0200
     1.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Mon May 02 22:52:15 2011 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  fun run_atp force_full_types timeout i n ctxt goal name =
     1.5    let
     1.6      val chained_ths = [] (* a tactic has no chained ths *)
     1.7 -    val params as {type_sys, relevance_thresholds, max_relevant, slicing, ...} =
     1.8 +    val params as {relevance_thresholds, max_relevant, slicing, ...} =
     1.9        ((if force_full_types then [("full_types", "true")] else [])
    1.10         @ [("timeout", string_of_int (Time.toSeconds timeout))])
    1.11         (* @ [("overlord", "true")] *)