# HG changeset patch
# User haftmann
# Date 1465241325 -7200
# Node ID 7c593d4f1f8944e56a406bf749f944391492157c
# Parent  3e908f762817eaec543104b48ffbee781a04fd38
dropped unused code

diff -r 3e908f762817 -r 7c593d4f1f89 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Jun 06 21:28:45 2016 +0200
+++ b/src/Pure/Isar/code.ML	Mon Jun 06 21:28:45 2016 +0200
@@ -49,8 +49,6 @@
   val add_eqn: thm -> theory -> theory
   val add_nbe_eqn: thm -> theory -> theory
   val add_abs_eqn: thm -> theory -> theory
-  val add_abs_eqn_attribute: attribute
-  val add_abs_eqn_attrib: Token.src
   val add_default_eqn: thm -> theory -> theory
   val add_default_eqn_attribute: attribute
   val add_default_eqn_attrib: Token.src
@@ -1139,12 +1137,8 @@
 fun add_abs_eqn raw_thm thy = gen_add_abs_eqn false (mk_abs_eqn thy raw_thm) thy;
 fun add_abs_default_eqn raw_thm thy = gen_add_abs_eqn true (mk_abs_eqn thy raw_thm) thy;
 
-val add_abs_eqn_attribute = Thm.declaration_attribute
-  (fn thm => Context.mapping (add_abs_eqn thm) I);
 val add_abs_default_eqn_attribute = Thm.declaration_attribute
   (fn thm => Context.mapping (add_abs_default_eqn thm) I);
-
-val add_abs_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
 val add_abs_default_eqn_attrib = Attrib.internal (K add_abs_default_eqn_attribute);
 
 fun add_eqn_maybe_abs thm thy =