Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Function/function_elims.ML
changeset 70479 02d08d0ba896
parent 67149 e61557884799
child 80634 a90ab1ea6458 
--- 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
isabelle