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/Pure/Isar/expression.ML
changeset 71017 c85efa2be619
parent 70622 2fb2e7661e16
child 71018 d32ed8927a42 
--- a/src/Pure/Isar/expression.ML	Sun Nov 03 19:43:59 2019 +0100
+++ b/src/Pure/Isar/expression.ML	Sun Nov 03 20:38:08 2019 +0100
@@ -720,7 +720,8 @@
         compose_tac defs_ctxt (false, body_eq RS Drule.equal_elim_rule1, 1) 1 THEN
         compose_tac defs_ctxt
           (false,
-            Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1);
+            Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1)
+      |> tap (Thm.expose_proof defs_thy);
 
     val conjuncts =
       (Drule.equal_elim_rule2 OF
isabelle