1.1 --- a/NEWS	Tue Mar 13 14:44:27 2012 +0100
     1.2 +++ b/NEWS	Tue Mar 13 16:22:18 2012 +0100
     1.3 @@ -43,6 +43,11 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Attribute "abs_def" turns an equation of the form "f x y == t" into
     1.8 +"f == %x y. t", which ensures that "simp" or "unfold" steps always
     1.9 +expand it.  This also works for object-logic equality.  (Formerly
    1.10 +undocumented feature.)
    1.11 +
    1.12  * Discontinued old "prems" fact, which used to refer to the accidental
    1.13  collection of foundational premises in the context (marked as legacy
    1.14  since Isabelle2011).

     2.1 --- a/src/Pure/Isar/attrib.ML	Tue Mar 13 14:44:27 2012 +0100
     2.2 +++ b/src/Pure/Isar/attrib.ML	Tue Mar 13 16:22:18 2012 +0100
     2.3 @@ -399,8 +399,10 @@
     2.4    setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
     2.5    setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del)
     2.6      "declaration of definitional transformations" #>
     2.7 -  setup (Binding.name "abs_def") (Scan.succeed (Thm.rule_attribute (K Drule.abs_def)))
     2.8 -    "abstract over free variables of a definition"));
     2.9 +  setup (Binding.name "abs_def")
    2.10 +    (Scan.succeed (Thm.rule_attribute (fn context =>
    2.11 +      Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
    2.12 +    "abstract over free variables of definitionial theorem"));
    2.13  
    2.14  
    2.15