diff -r 17b2aad869fa -r 1796b8ea88aa src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Mar 13 21:24:21 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Fri Mar 13 21:25:15 2009 +0100
@@ -24,14 +24,13 @@
     (('c * 'att list) * ('d * 'att list) list) list
   val crude_closure: Proof.context -> src -> src
   val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
-  val syntax: (Context.generic * Args.T list ->
-    attribute * (Context.generic * Args.T list)) -> src -> attribute
+  val syntax: attribute context_parser -> src -> attribute
   val no_args: attribute -> src -> attribute
   val add_del_args: attribute -> attribute -> src -> attribute
-  val thm_sel: Args.T list -> Facts.interval list * Args.T list
-  val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list)
-  val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
-  val multi_thm: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
+  val thm_sel: Facts.interval list parser
+  val thm: thm context_parser
+  val thms: thm list context_parser
+  val multi_thm: thm list context_parser
   val print_configs: Proof.context -> unit
   val internal: (morphism -> attribute) -> src
   val register_config: Config.value Config.T -> theory -> theory