merged
authorwenzelm
Wed, 08 Apr 2020 14:48:55 +0200
changeset 71948 ada8812f5a9e
parent 71944 c986a422dee1 (current diff)
parent 71947 d8e60a0ffa02 (diff)
child 71953 7ff701556063
merged
--- 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;