--- 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
--- 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;