changeset 54141 | f57f8e7a879f |
parent 54126 | 6675cdc0d1ae |
child 55198 | 7a538e58b64e |
--- a/src/HOL/TPTP/sledgehammer_tactics.ML Thu Oct 17 20:20:53 2013 +0200 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML Thu Oct 17 20:49:19 2013 +0200 @@ -42,7 +42,7 @@ concl_t |> hd |> snd val problem = - {state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, + {comment = "", state = Proof.init ctxt, goal = goal, subgoal = i, subgoal_count = n, factss = [("", facts)]} in (case prover params (K (K (K ""))) problem of