--- 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 =