src/Pure/Isar/attrib.ML
changeset 30513 1796b8ea88aa
parent 30466 5f31e24937c5
child 30525 8a5a0aa30e1c
     1.1 --- a/src/Pure/Isar/attrib.ML	Fri Mar 13 21:24:21 2009 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Fri Mar 13 21:25:15 2009 +0100
     1.3 @@ -24,14 +24,13 @@
     1.4      (('c * 'att list) * ('d * 'att list) list) list
     1.5    val crude_closure: Proof.context -> src -> src
     1.6    val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
     1.7 -  val syntax: (Context.generic * Args.T list ->
     1.8 -    attribute * (Context.generic * Args.T list)) -> src -> attribute
     1.9 +  val syntax: attribute context_parser -> src -> attribute
    1.10    val no_args: attribute -> src -> attribute
    1.11    val add_del_args: attribute -> attribute -> src -> attribute
    1.12 -  val thm_sel: Args.T list -> Facts.interval list * Args.T list
    1.13 -  val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list)
    1.14 -  val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
    1.15 -  val multi_thm: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
    1.16 +  val thm_sel: Facts.interval list parser
    1.17 +  val thm: thm context_parser
    1.18 +  val thms: thm list context_parser
    1.19 +  val multi_thm: thm list context_parser
    1.20    val print_configs: Proof.context -> unit
    1.21    val internal: (morphism -> attribute) -> src
    1.22    val register_config: Config.value Config.T -> theory -> theory