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/legacy_transfer.ML
changeset 66795 420d0080545f
parent 61853 fb7756087101 
--- a/src/HOL/Tools/legacy_transfer.ML	Mon Oct 09 16:14:18 2017 +0100
+++ b/src/HOL/Tools/legacy_transfer.ML	Sun Oct 08 22:28:19 2017 +0200
@@ -154,7 +154,6 @@
     { inj = inj1, embed = embed1, return = return1, cong = cong1, hints = hints1 }
     { inj = inj2, embed = embed2, return = return2, cong = cong2, hints = hints2 } =
   let
-    fun add_del eq del add = union eq add #> subtract eq del;
     val guessed = if guess
       then map (fn thm => transfer_thm
         ((a, D), (if null inj1 then inj2 else inj1, [], [], cong1)) [] ctxt thm RS sym) embed1
isabelle