src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML

     val facts =
       facts |> maps (fn (n, ths) => ths |> map (Untranslated_Fact o pair n))
     val {goal, ...} = Proof.goal state
     val problem =
       {state = state, goal = goal, subgoal = i, subgoal_count = n,
-       facts = facts}
+       facts = facts, smt_head = NONE}
     val result as {outcome, used_facts, ...} = prover params (K "") problem
   in
     print silent
         (fn () => case outcome of
                     SOME failure => string_for_failure failure