diff -r 94ed5be08e7f -r 02d08d0ba896 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Wed Aug 07 10:31:54 2019 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Wed Aug 07 10:42:34 2019 +0200
@@ -263,6 +263,7 @@
     |> Tactic.rule_by_tactic ctxt (ALLGOALS prep_subgoal_tac)
     |> Thm.forall_intr x
     |> Thm.forall_intr P
+    |> Thm.solve_constraints
   end