# HG changeset patch
# User kuncar
# Date 1393261959 -3600
# Node ID f3a2931a66568dc05270d83e0c4334417f2c980f
# Parent  cdddd073bff81a6cbec22328994daa8e8d5f6e6b
add missing attributes

diff -r cdddd073bff8 -r f3a2931a6656 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Mon Feb 24 16:56:04 2014 +0000
+++ b/src/Pure/Isar/code.ML	Mon Feb 24 18:12:39 2014 +0100
@@ -47,6 +47,8 @@
   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: Attrib.src
   val add_default_eqn: thm -> theory -> theory
   val add_default_eqn_attribute: attribute
   val add_default_eqn_attrib: Attrib.src
@@ -1121,6 +1123,10 @@
 
 fun add_abs_eqn raw_thm thy = gen_add_abs_eqn (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_eqn_attrib = Attrib.internal (K add_abs_eqn_attribute);
+
 fun add_eqn_maybe_abs thm thy =
   case mk_eqn_maybe_abs thy thm
    of SOME (eqn, NONE) => gen_add_eqn false eqn thy