more robust: notably for sledgehammer with 'using' and prover=cvc4;
authorwenzelm
Sat, 04 Apr 2020 22:39:42 +0200
changeset 71945 8ed68b2aeba1
parent 71880 9fdbd2f0b56e
child 71946 5e810ff0346d
more robust: notably for sledgehammer with 'using' and prover=cvc4;
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;