# HG changeset patch
# User wenzelm
# Date 1237412474 -3600
# Node ID 368e26dfba6931543fd754294142cf15ed84f7c8
# Parent  b9bcc640ed586e0ad00e764ad8acc6029f1d0bc9
more precise type Symbol_Pos.text;

diff -r b9bcc640ed58 -r 368e26dfba69 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Wed Mar 18 22:41:14 2009 +0100
+++ b/src/Pure/Isar/attrib.ML	Wed Mar 18 22:41:14 2009 +0100
@@ -26,7 +26,8 @@
   val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
   val syntax: attribute context_parser -> src -> attribute
   val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
-  val attribute_setup: bstring * Position.T -> string * Position.T -> string -> theory -> theory
+  val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
+    theory -> theory
   val no_args: attribute -> src -> attribute
   val add_del: attribute -> attribute -> attribute context_parser
   val add_del_args: attribute -> attribute -> src -> attribute
diff -r b9bcc640ed58 -r 368e26dfba69 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Mar 18 22:41:14 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Mar 18 22:41:14 2009 +0100
@@ -6,18 +6,18 @@
 
 signature ISAR_CMD =
 sig
-  val global_setup: string * Position.T -> theory -> theory
-  val local_setup: string * Position.T -> Proof.context -> Proof.context
-  val parse_ast_translation: bool * (string * Position.T) -> theory -> theory
-  val parse_translation: bool * (string * Position.T) -> theory -> theory
-  val print_translation: bool * (string * Position.T) -> theory -> theory
-  val typed_print_translation: bool * (string * Position.T) -> theory -> theory
-  val print_ast_translation: bool * (string * Position.T) -> theory -> theory
+  val global_setup: Symbol_Pos.text * Position.T -> theory -> theory
+  val local_setup: Symbol_Pos.text * Position.T -> Proof.context -> Proof.context
+  val parse_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+  val parse_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+  val print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+  val typed_print_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
+  val print_ast_translation: bool * (Symbol_Pos.text * Position.T) -> theory -> theory
   val oracle: bstring * Position.T -> Symbol_Pos.text * Position.T -> theory -> theory
   val add_axioms: ((binding * string) * Attrib.src list) list -> theory -> theory
   val add_defs: (bool * bool) * ((binding * string) * Attrib.src list) list -> theory -> theory
-  val declaration: string * Position.T -> local_theory -> local_theory
-  val simproc_setup: string -> string list -> string * Position.T -> string list ->
+  val declaration: Symbol_Pos.text * Position.T -> local_theory -> local_theory
+  val simproc_setup: string -> string list -> Symbol_Pos.text * Position.T -> string list ->
     local_theory -> local_theory
   val hide_names: bool -> string * xstring list -> theory -> theory
   val have: (Attrib.binding * (string * string list) list) list -> bool -> Proof.state -> Proof.state
@@ -38,7 +38,7 @@
   val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
   val disable_pr: Toplevel.transition -> Toplevel.transition
   val enable_pr: Toplevel.transition -> Toplevel.transition
-  val ml_diag: bool -> string * Position.T -> Toplevel.transition -> Toplevel.transition
+  val ml_diag: bool -> Symbol_Pos.text * Position.T -> Toplevel.transition -> Toplevel.transition
   val cd: Path.T -> Toplevel.transition -> Toplevel.transition
   val pwd: Toplevel.transition -> Toplevel.transition
   val display_drafts: Path.T list -> Toplevel.transition -> Toplevel.transition
diff -r b9bcc640ed58 -r 368e26dfba69 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Wed Mar 18 22:41:14 2009 +0100
+++ b/src/Pure/Isar/method.ML	Wed Mar 18 22:41:14 2009 +0100
@@ -81,7 +81,8 @@
     -> theory -> theory
   val syntax: 'a context_parser -> src -> Proof.context -> 'a * Proof.context
   val setup: binding -> (Proof.context -> method) context_parser -> string -> theory -> theory
-  val method_setup: bstring * Position.T -> string * Position.T -> string -> theory -> theory
+  val method_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
+    theory -> theory
   val simple_args: 'a parser -> ('a -> Proof.context -> method) -> src -> Proof.context -> method
   val ctxt_args: (Proof.context -> method) -> src -> Proof.context -> method
   val no_args: method -> src -> Proof.context -> method