--- 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;