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 71018 d32ed8927a42
parent 71017 c85efa2be619
child 71019 c9f5f724abc0 
--- a/src/Pure/Isar/expression.ML	Sun Nov 03 20:38:08 2019 +0100
+++ b/src/Pure/Isar/expression.ML	Mon Nov 04 14:56:49 2019 +0100
@@ -720,8 +720,7 @@
         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)
-      |> tap (Thm.expose_proof defs_thy);
+            Conjunction.intr_balanced (map (Thm.assume o Thm.cterm_of defs_ctxt) norm_ts), 0) 1);
 
     val conjuncts =
       (Drule.equal_elim_rule2 OF
isabelle