# HG changeset patch
# User wenzelm
# Date 1138559026 -3600
# Node ID 86a59812b03bb63b39e6491c7e5effae9cc0f73d
# Parent  d32f707893429e8d09043f4648a99c557cf84261
added 'defn' attribute;
attribute (un)folded: option '(raw)';

diff -r d32f70789342 -r 86a59812b03b src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Jan 29 19:23:45 2006 +0100
+++ b/src/Pure/Isar/attrib.ML	Sun Jan 29 19:23:46 2006 +0100
@@ -396,8 +396,12 @@
 
 (* unfold / fold definitions *)
 
-val unfolded = syntax (thmss >> (fn defs => Thm.rule_attribute (K (ObjectLogic.unfold defs))));
-val folded = syntax (thmss >> (fn defs => Thm.rule_attribute (K (ObjectLogic.fold defs))));
+fun unfolded_syntax rule =
+  syntax ((Args.mode "raw" >> not) -- thmss >>
+    (fn (b, ths) => Thm.rule_attribute (fn context => rule (Context.proof_of context) b ths)));
+
+val unfolded = unfolded_syntax LocalDefs.unfold;
+val folded = unfolded_syntax LocalDefs.fold;
 
 
 (* rule cases *)
@@ -455,6 +459,8 @@
     ("atomize", no_args ObjectLogic.declare_atomize, "declaration of atomize rule"),
     ("rulify", no_args ObjectLogic.declare_rulify, "declaration of rulify rule"),
     ("rule_format", rule_format_att, "result put into standard rule format"),
+    ("defn", add_del_args LocalDefs.defn_add LocalDefs.defn_del,
+      "declaration of definitional transformations"),
     ("attribute", internal_att, "internal attribute")]);
 
 end;