src/Pure/Isar/attrib.ML
changeset 46903 3d44892ac0d6
parent 46775 6287653e63ec
child 46906 3c1787d46935
--- 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"));