# HG changeset patch
# User wenzelm
# Date 1138727967 -3600
# Node ID 020044cf15100517bae2acf638d06686fc3681e8
# Parent  ca48320f661966d805fc5c57cc8a8c9044bb0acc
(un)folded: removed '(raw)' option;

diff -r ca48320f6619 -r 020044cf1510 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Tue Jan 31 18:19:26 2006 +0100
+++ b/src/Pure/Isar/attrib.ML	Tue Jan 31 18:19:27 2006 +0100
@@ -397,8 +397,8 @@
 (* unfold / fold definitions *)
 
 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)));
+  syntax (thmss >>
+    (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths)));
 
 val unfolded = unfolded_syntax LocalDefs.unfold;
 val folded = unfolded_syntax LocalDefs.fold;