more careful treatment of implicit context;
authorwenzelm
Wed, 07 Aug 2019 10:42:34 +0200
changeset 70665 02d08d0ba896
parent 70664 94ed5be08e7f
child 70666 1a1b7d7f24bb
more careful treatment of implicit context;
src/HOL/Tools/Function/function_elims.ML
src/HOL/Tools/Function/mutual.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
--- 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