diff -r 6ed6112f0a95 -r bafd82950e24 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon May 03 07:59:51 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon May 03 14:25:56 2010 +0200
@@ -850,10 +850,10 @@
 val read_term = singleton o read_terms;
 val read_prop = singleton o read_props;
 
-val read_sort_global = read_sort o ProofContext.init;
-val read_typ_global = read_typ o ProofContext.init;
-val read_term_global = read_term o ProofContext.init;
-val read_prop_global = read_prop o ProofContext.init;
+val read_sort_global = read_sort o ProofContext.init_global;
+val read_typ_global = read_typ o ProofContext.init_global;
+val read_term_global = read_term o ProofContext.init_global;
+val read_prop_global = read_prop o ProofContext.init_global;
 
 
 (* pretty = uncheck + unparse *)
@@ -876,7 +876,7 @@
 structure PrettyGlobal = Proof_Data(type T = bool fun init _ = false);
 val is_pretty_global = PrettyGlobal.get;
 val set_pretty_global = PrettyGlobal.put;
-val init_pretty_global = set_pretty_global true o ProofContext.init;
+val init_pretty_global = set_pretty_global true o ProofContext.init_global;
 
 val pretty_term_global = pretty_term o init_pretty_global;
 val pretty_typ_global = pretty_typ o init_pretty_global;