1.1 --- a/src/Pure/Isar/attrib.ML	Wed Mar 18 22:41:14 2009 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Wed Mar 18 22:41:14 2009 +0100
     1.3 @@ -26,7 +26,8 @@
     1.4    val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
     1.5    val syntax: attribute context_parser -> src -> attribute
     1.6    val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
     1.7 -  val attribute_setup: bstring * Position.T -> string * Position.T -> string -> theory -> theory
     1.8 +  val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
     1.9 +    theory -> theory
    1.10    val no_args: attribute -> src -> attribute
    1.11    val add_del: attribute -> attribute -> attribute context_parser
    1.12    val add_del_args: attribute -> attribute -> src -> attribute

     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Wed Mar 18 22:41:14 2009 +0100
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 18 22:41:14 2009 +0100
     2.3 @@ -6,18 +6,18 @@
     2.4  
     2.5  signature ISAR_CMD =
     2.6  sig
     2.7 -  val global_setup: string * Position.T -> theory -> theory
     2.8 -  val local_setup: string * Position.T -> Proof.context -> Proof.context
     2.9 -  val parse_ast_translation: bool * (string * Position.T) -> theory -> theory
    2.10 -  val parse_translation: bool * (string * Position.T) -> theory -> theory
    2.11 -  val print_translation: bool * (string * Position.T) -> theory -> theory
    2.12 -  val typed_print_translation: bool * (string * Position.T) -> theory -> theory
    2.13 -  val print_ast_translation: bool * (string * Position.T) -> theory -> theory
    2.14 +  val global_setup: Symbol_Pos.text * Position.T -> theory -> theory
    2.15 +  val local_setup: Symbol_Pos.text * Position.T -> Proof.context -> Proof.context
    2.16 +  val parse_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
    2.17 +  val parse_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
    2.18 +  val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
    2.19 +  val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
    2.20 +  val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
    2.21    val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
    2.22    val add_axioms: ((binding * string) * Attrib.src list) list -> theory -> theory
    2.23    val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
    2.24 -  val declaration: string * Position.T -> local_theory -> local_theory
    2.25 -  val simproc_setup: string -> string list -> string * Position.T -> string list ->
    2.26 +  val declaration: Symbol_Pos.text * Position.T -> local_theory -> local_theory
    2.27 +  val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
    2.28      local_theory -> local_theory
    2.29    val hide_names: bool -> string * xstring list -> theory -> theory
    2.30    val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
    2.31 @@ -38,7 +38,7 @@
    2.32    val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
    2.33    val disable_pr: Toplevel.transition -> Toplevel.transition
    2.34    val enable_pr: Toplevel.transition -> Toplevel.transition
    2.35 -  val ml_diag: bool -> string * Position.T -> Toplevel.transition -> Toplevel.transition
    2.36 +  val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
    2.37    val cd: Path.T -> Toplevel.transition -> Toplevel.transition
    2.38    val pwd: Toplevel.transition -> Toplevel.transition
    2.39    val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition

     3.1 --- a/src/Pure/Isar/method.ML	Wed Mar 18 22:41:14 2009 +0100
     3.2 +++ b/src/Pure/Isar/method.ML	Wed Mar 18 22:41:14 2009 +0100
     3.3 @@ -81,7 +81,8 @@
     3.4      -> theory -> theory
     3.5    val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
     3.6    val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
     3.7 -  val method_setup: bstring * Position.T -> string * Position.T -> string -> theory -> theory
     3.8 +  val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
     3.9 +    theory -> theory
    3.10    val simple_args: 'a parser -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
    3.11    val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
    3.12    val no_args: method -> src -> Proof.context -> method