1.1 --- a/src/Pure/Syntax/syntax.ML	Tue Sep 25 13:28:41 2007 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Tue Sep 25 13:28:42 2007 +0200
     1.3 @@ -95,10 +95,6 @@
     1.4    val parse_typ: Proof.context -> string -> typ
     1.5    val parse_term: Proof.context -> string -> term
     1.6    val parse_prop: Proof.context -> string -> term
     1.7 -  val global_parse_sort: theory -> string -> sort
     1.8 -  val global_parse_typ: theory -> string -> typ
     1.9 -  val global_parse_term: theory -> string -> term
    1.10 -  val global_parse_prop: theory -> string -> term
    1.11    val check_sort: Proof.context -> sort -> sort
    1.12    val check_typ: Proof.context -> typ -> typ
    1.13    val check_term: Proof.context -> term -> term
    1.14 @@ -116,10 +112,10 @@
    1.15    val read_prop: Proof.context -> string -> term
    1.16    val read_terms: Proof.context -> string list -> term list
    1.17    val read_props: Proof.context -> string list -> term list
    1.18 -  val global_read_sort: theory -> string -> sort
    1.19 -  val global_read_typ: theory -> string -> typ
    1.20 -  val global_read_term: theory -> string -> term
    1.21 -  val global_read_prop: theory -> string -> term
    1.22 +  val read_sort_global: theory -> string -> sort
    1.23 +  val read_typ_global: theory -> string -> typ
    1.24 +  val read_term_global: theory -> string -> term
    1.25 +  val read_prop_global: theory -> string -> term
    1.26  end;
    1.27  
    1.28  structure Syntax: SYNTAX =
    1.29 @@ -634,11 +630,6 @@
    1.30  val parse_term = parse #term;
    1.31  val parse_prop = parse #prop;
    1.32  
    1.33 -val global_parse_sort = parse_sort o ProofContext.init;
    1.34 -val global_parse_typ = parse_typ o ProofContext.init;
    1.35 -val global_parse_term = parse_term o ProofContext.init;
    1.36 -val global_parse_prop = parse_prop o ProofContext.init;
    1.37 -
    1.38  
    1.39  (* checking types/terms *)
    1.40  
    1.41 @@ -702,10 +693,10 @@
    1.42  val read_term = singleton o read_terms;
    1.43  val read_prop = singleton o read_props;
    1.44  
    1.45 -val global_read_sort = read_sort o ProofContext.init;
    1.46 -val global_read_typ = read_typ o ProofContext.init;
    1.47 -val global_read_term = read_term o ProofContext.init;
    1.48 -val global_read_prop = read_prop o ProofContext.init;
    1.49 +val read_sort_global = read_sort o ProofContext.init;
    1.50 +val read_typ_global = read_typ o ProofContext.init;
    1.51 +val read_term_global = read_term o ProofContext.init;
    1.52 +val read_prop_global = read_prop o ProofContext.init;
    1.53  
    1.54  
    1.55  (*export parts of internal Syntax structures*)