src/Pure/Syntax/syntax.ML
changeset 36610 bafd82950e24
parent 36208 74c5e6e3c1d3
child 36739 e9401d2efc5f
     1.1 --- a/src/Pure/Syntax/syntax.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/Pure/Syntax/syntax.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -850,10 +850,10 @@
     1.4  val read_term = singleton o read_terms;
     1.5  val read_prop = singleton o read_props;
     1.6  
     1.7 -val read_sort_global = read_sort o ProofContext.init;
     1.8 -val read_typ_global = read_typ o ProofContext.init;
     1.9 -val read_term_global = read_term o ProofContext.init;
    1.10 -val read_prop_global = read_prop o ProofContext.init;
    1.11 +val read_sort_global = read_sort o ProofContext.init_global;
    1.12 +val read_typ_global = read_typ o ProofContext.init_global;
    1.13 +val read_term_global = read_term o ProofContext.init_global;
    1.14 +val read_prop_global = read_prop o ProofContext.init_global;
    1.15  
    1.16  
    1.17  (* pretty = uncheck + unparse *)
    1.18 @@ -876,7 +876,7 @@
    1.19  structure PrettyGlobal = Proof_Data(type T = bool fun init _ = false);
    1.20  val is_pretty_global = PrettyGlobal.get;
    1.21  val set_pretty_global = PrettyGlobal.put;
    1.22 -val init_pretty_global = set_pretty_global true o ProofContext.init;
    1.23 +val init_pretty_global = set_pretty_global true o ProofContext.init_global;
    1.24  
    1.25  val pretty_term_global = pretty_term o init_pretty_global;
    1.26  val pretty_typ_global = pretty_typ o init_pretty_global;