# HG changeset patch
# User webertj
# Date 1360579096 -3600
# Node ID 36aee533d7a772fcda4a83916f5a8c60dad754b5
# Parent  0ee6039d2c8e3e887b709b10d3698975a5ce307a
Typo in description of abs_def.

diff -r 0ee6039d2c8e -r 36aee533d7a7 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Feb 08 16:41:04 2013 +0100
+++ b/src/Pure/Isar/attrib.ML	Mon Feb 11 11:38:16 2013 +0100
@@ -420,7 +420,7 @@
   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"));
+    "abstract over free variables of definitional theorem"));