Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more careful treatment of implicit context;
authorwenzelm
Wed, 07 Aug 2019 10:42:34 +0200
changeset 70479 02d08d0ba896
parent 70478 94ed5be08e7f
child 70480 1a1b7d7f24bb
more careful treatment of implicit context;
src/HOL/Tools/Function/function_elims.ML file | annotate | diff | comparison | revisions
src/HOL/Tools/Function/mutual.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle