more robust: notably for sledgehammer with 'using' and prover=cvc4;

--- a/src/Pure/Isar/subgoal.ML	Thu Apr 02 11:45:03 2020 +0200
+++ b/src/Pure/Isar/subgoal.ML	Sat Apr 04 22:39:42 2020 +0200
@@ -44,6 +44,7 @@
 fun gen_focus (do_prems, do_concl) ctxt i bindings raw_st =
   let
     val st = raw_st
+      |> Thm.solve_constraints
       |> Thm.transfer' ctxt
       |> Raw_Simplifier.norm_hhf_protect ctxt;
     val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;