# HG changeset patch
# User wenzelm
# Date 1586032782 -7200
# Node ID 8ed68b2aeba19ea47f1e38038ac87a32c17161ce
# Parent  9fdbd2f0b56e1eceb6d01178a34194e9ba92441e
more robust: notably for sledgehammer with 'using' and prover=cvc4;

diff -r 9fdbd2f0b56e -r 8ed68b2aeba1 src/Pure/Isar/subgoal.ML
--- 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;