# HG changeset patch
# User wenzelm
# Date 1586350135 -7200
# Node ID ada8812f5a9ede7ce0d9248149f1a4ef8a8acb0f
# Parent  c986a422dee1852c8df40935e7514e7f914c9050# Parent  d8e60a0ffa02e0370bf8bc8b6c6937c71c009d8f
merged

diff -r c986a422dee1 -r ada8812f5a9e .hgtags
--- a/.hgtags	Tue Apr 07 22:13:22 2020 +0200
+++ b/.hgtags	Wed Apr 08 14:48:55 2020 +0200
@@ -41,3 +41,4 @@
 7eadccd4392cc1f3b603c0fa5734d0629f039cc0 Isabelle2020-RC2
 7fe1a344404a9f7e6e4cdef584338c6d9849812c Isabelle2020-RC3
 1f3d9a9dd42a9543af7062ca08a36da2c5375454 Isabelle2020-RC4
+8ed68b2aeba19ea47f1e38038ac87a32c17161ce Isabelle2020-RC5
diff -r c986a422dee1 -r ada8812f5a9e src/Pure/Isar/subgoal.ML
--- a/src/Pure/Isar/subgoal.ML	Tue Apr 07 22:13:22 2020 +0200
+++ b/src/Pure/Isar/subgoal.ML	Wed Apr 08 14:48:55 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;