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