# HG changeset patch
# User wenzelm
# Date 1565167354 -7200
# Node ID 02d08d0ba8966a7f967f8d6a8a6b617191cd6ace
# Parent  94ed5be08e7fec592ac7ef37ea83ffa41c745e79
more careful treatment of implicit context;

diff -r 94ed5be08e7f -r 02d08d0ba896 src/HOL/Tools/Function/function_elims.ML
--- a/src/HOL/Tools/Function/function_elims.ML	Wed Aug 07 10:31:54 2019 +0200
+++ b/src/HOL/Tools/Function/function_elims.ML	Wed Aug 07 10:42:34 2019 +0200
@@ -146,7 +146,7 @@
           |> fold_rev (Thm.forall_intr o Thm.cterm_of ctxt) arg_vars
           |> Thm.forall_intr P
       in
-        map unstrip (elim_stripped :: bool_elims)
+        map (unstrip #> Thm.solve_constraints) (elim_stripped :: bool_elims)
       end;
   in
     map_index mk_partial_elim_rule fs
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