src/HOL/ex/sledgehammer_tactics.ML
changeset 43051 d7075adac3bd
parent 43021 5910dd009d0e
child 43088 0a97f3295642
     1.1 --- a/src/HOL/ex/sledgehammer_tactics.ML	Mon May 30 17:00:38 2011 +0200
     1.2 +++ b/src/HOL/ex/sledgehammer_tactics.ML	Mon May 30 17:00:38 2011 +0200
     1.3 @@ -43,7 +43,7 @@
     1.4         facts = map Sledgehammer_Provers.Untranslated_Fact facts,
     1.5         smt_filter = NONE}
     1.6    in
     1.7 -    (case prover params (K "") problem of
     1.8 +    (case prover params (K (K "")) problem of
     1.9        {outcome = NONE, used_facts, ...} => used_facts |> map fst |> SOME
    1.10      | _ => NONE)
    1.11        handle ERROR message => (warning ("Error: " ^ message ^ "\n"); NONE)