diff -r 0a8a75e400da -r 8b9401bfd9fd src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Apr 28 11:47:01 2016 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Apr 28 15:42:52 2016 +0200
@@ -581,8 +581,7 @@
     (add_del Local_Defs.defn_add Local_Defs.defn_del)
     "declaration of definitional transformations" #>
   setup @{binding abs_def}
-    (Scan.succeed (Thm.rule_attribute [] (fn context =>
-      Local_Defs.meta_rewrite_rule (Context.proof_of context) #> Drule.abs_def)))
+    (Scan.succeed (Thm.rule_attribute [] (Local_Defs.abs_def_rule o Context.proof_of)))
     "abstract over free variables of definitional theorem" #>
 
   register_config Goal.quick_and_dirty_raw #>
@@ -619,7 +618,8 @@
   register_config Raw_Simplifier.simp_depth_limit_raw #>
   register_config Raw_Simplifier.simp_trace_depth_limit_raw #>
   register_config Raw_Simplifier.simp_debug_raw #>
-  register_config Raw_Simplifier.simp_trace_raw);
+  register_config Raw_Simplifier.simp_trace_raw #>
+  register_config Local_Defs.unfold_abs_def_raw);
 
 
 (* internal source *)