# HG changeset patch
# User haftmann
# Date 1507494499 -7200
# Node ID 420d0080545fd9c420fe8a4c1d5b2159ca8c5ac6
# Parent  83bf64da6938ba227ed6e0d617648ff060b6945b
dropped dead code

diff -r 83bf64da6938 -r 420d0080545f src/HOL/Nat_Transfer.thy
--- a/src/HOL/Nat_Transfer.thy	Mon Oct 09 16:14:18 2017 +0100
+++ b/src/HOL/Nat_Transfer.thy	Sun Oct 08 22:28:19 2017 +0200
@@ -285,7 +285,7 @@
     "(int x) * (int y) = int (x * y)"
     "tsub (int x) (int y) = int (x - y)"
     "(int x)^n = int (x^n)"
-  by (auto simp add: of_nat_mult tsub_def of_nat_power)
+  by (auto simp add: tsub_def)
 
 lemma transfer_int_nat_function_closures:
     "is_nat x \<Longrightarrow> is_nat y \<Longrightarrow> is_nat (x + y)"
diff -r 83bf64da6938 -r 420d0080545f src/HOL/Tools/legacy_transfer.ML
--- 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