# HG changeset patch
# User wenzelm
# Date 1185652861 -7200
# Node ID d39d64d96e7163226e8f5a18b29d47dbcab61615
# Parent  9221b600dbb2de68213fac913ad079c6873eab2a
attribute "option": proper naming within the theory

diff -r 9221b600dbb2 -r d39d64d96e71 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat Jul 28 22:01:00 2007 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat Jul 28 22:01:01 2007 +0200
@@ -203,19 +203,20 @@
   | scan_value (ConfigOption.Int _) = (equals |-- Args.int) >> ConfigOption.Int
   | scan_value (ConfigOption.String _) = (equals |-- Args.name) >> ConfigOption.String;
 
-fun scan_config x =
-  ((Args.name >> ConfigOption.the_option) :|-- (fn (config, config_type) =>
+fun scan_config thy =
+  (Args.name >> ConfigOption.the_option thy) :|-- (fn (config, config_type) =>
     scan_value config_type >> (fn value =>
-      K (Thm.declaration_attribute (K (ConfigOption.put_generic config value)))))) x;
+      K (Thm.declaration_attribute (K (ConfigOption.put_generic config value)))));
 
-fun scan_att x =
+fun scan_att thy =
   (Args.internal_attribute ||
-    (Scan.ahead (scan_config --| Args.terminator) :|--
-      (fn att => Args.named_attribute (K att)))) x;
+    (Scan.ahead (scan_config thy --| Args.terminator) :|--
+      (fn att => Args.named_attribute (K att))));
 
 in
 
-fun option x = syntax (Scan.lift ((scan_att >> Morphism.form) --| Scan.many Args.not_eof)) x;
+fun option x = syntax (Scan.peek (fn context =>
+  (scan_att (Context.theory_of context) >> Morphism.form) --| Scan.many Args.not_eof)) x;
 
 end;