# HG changeset patch
# User wenzelm
# Date 1331652138 -3600
# Node ID 3d44892ac0d64c5b5d003a40f64d1301b1b6e472
# Parent  8d1b9acad2871d2433b4a56c985de57b5adc891f
improved attribute "abs_def" to handle object-equality as well;

diff -r 8d1b9acad287 -r 3d44892ac0d6 NEWS
--- a/NEWS	Tue Mar 13 14:44:27 2012 +0100
+++ b/NEWS	Tue Mar 13 16:22:18 2012 +0100
@@ -43,6 +43,11 @@
 
 *** Pure ***
 
+* Attribute "abs_def" turns an equation of the form "f x y == t" into
+"f == %x y. t", which ensures that "simp" or "unfold" steps always
+expand it.  This also works for object-logic equality.  (Formerly
+undocumented feature.)
+
 * Discontinued old "prems" fact, which used to refer to the accidental
 collection of foundational premises in the context (marked as legacy
 since Isabelle2011).
diff -r 8d1b9acad287 -r 3d44892ac0d6 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Mar 13 14:44:27 2012 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Mar 13 16:22:18 2012 +0100
@@ -399,8 +399,10 @@
   setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
   setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del)
     "declaration of definitional transformations" #>
-  setup (Binding.name "abs_def") (Scan.succeed (Thm.rule_attribute (K Drule.abs_def)))
-    "abstract over free variables of a definition"));
+  setup (Binding.name "abs_def")
+    (Scan.succeed (Thm.rule_attribute (fn context =>
+      Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
+    "abstract over free variables of definitionial theorem"));