author | blanchet |
Mon, 30 Aug 2010 11:10:44 +0200 | |
changeset 38893 | aa21c33a104f |
parent 38892 | eccc9e2a6412 |
child 38894 | e85263e281be |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 30 10:26:17 2010 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML Mon Aug 30 11:10:44 2010 +0200 @@ -219,7 +219,7 @@ ({subgoal, goal = (ctxt, (chained_ths, th)), relevance_override, axioms} : problem) = let - val (params, hyp_ts, concl_t) = strip_subgoal th subgoal + val (_, hyp_ts, concl_t) = strip_subgoal th subgoal val print = priority fun print_v f = () |> verbose ? print o f