diff -r 148c8aba89dd -r 7c7ade4f537b src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Dec 11 19:05:25 2006 +0100
+++ b/src/Pure/sign.ML	Mon Dec 11 21:39:26 2006 +0100
@@ -36,12 +36,12 @@
   val add_trfunsT:
     (string * (bool -> typ -> term list -> term)) list -> theory -> theory
   val add_advanced_trfuns:
-    (string * (Context.generic -> ast list -> ast)) list *
-    (string * (Context.generic -> term list -> term)) list *
-    (string * (Context.generic -> term list -> term)) list *
-    (string * (Context.generic -> ast list -> ast)) list -> theory -> theory
+    (string * (Proof.context -> ast list -> ast)) list *
+    (string * (Proof.context -> term list -> term)) list *
+    (string * (Proof.context -> term list -> term)) list *
+    (string * (Proof.context -> ast list -> ast)) list -> theory -> theory
   val add_advanced_trfunsT:
-    (string * (Context.generic -> bool -> typ -> term list -> term)) list -> theory -> theory
+    (string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory
   val add_tokentrfuns:
     (string * string * (string -> string * real)) list -> theory -> theory
   val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list
@@ -133,7 +133,7 @@
   val intern_term: theory -> term -> term
   val extern_term: (string -> xstring) -> theory -> term -> term
   val intern_tycons: theory -> typ -> typ
-  val pretty_term': Context.generic -> Syntax.syntax -> (string -> xstring) -> term -> Pretty.T
+  val pretty_term': Proof.context -> Syntax.syntax -> (string -> xstring) -> term -> Pretty.T
   val pretty_term: theory -> term -> Pretty.T
   val pretty_typ: theory -> typ -> Pretty.T
   val pretty_sort: theory -> sort -> Pretty.T
@@ -161,15 +161,14 @@
   val no_vars: Pretty.pp -> term -> term
   val cert_def: Pretty.pp -> term -> (string * typ) * term
   val read_class: theory -> xstring -> class
-  val read_sort': Syntax.syntax -> Context.generic -> string -> sort
+  val read_sort': Syntax.syntax -> Proof.context -> string -> sort
   val read_sort: theory -> string -> sort
   val read_arity: theory -> xstring * string list * string -> arity
   val cert_arity: theory -> arity -> arity
-  val read_typ': Syntax.syntax -> Context.generic ->
+  val read_typ': Syntax.syntax -> Proof.context -> (indexname -> sort option) -> string -> typ
+  val read_typ_syntax': Syntax.syntax -> Proof.context ->
     (indexname -> sort option) -> string -> typ
-  val read_typ_syntax': Syntax.syntax -> Context.generic ->
-    (indexname -> sort option) -> string -> typ
-  val read_typ_abbrev': Syntax.syntax -> Context.generic ->
+  val read_typ_abbrev': Syntax.syntax -> Proof.context ->
     (indexname -> sort option) -> string -> typ
   val read_typ: theory * (indexname -> sort option) -> string -> typ
   val read_typ_syntax: theory * (indexname -> sort option) -> string -> typ
@@ -183,7 +182,7 @@
     (indexname -> sort option) -> Name.context -> bool
     -> term list * typ -> term * (indexname * typ) list
   val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax -> Consts.T ->
-    Context.generic -> (indexname -> typ option) * (indexname -> sort option) ->
+    Proof.context -> (indexname -> typ option) * (indexname -> sort option) ->
     Name.context -> bool -> (string * typ) list -> term list * (indexname * typ) list
   val read_def_terms:
     theory * (indexname -> typ option) * (indexname -> sort option) ->
@@ -371,16 +370,19 @@
 
 (** pretty printing of terms, types etc. **)
 
-fun pretty_term' context syn ext t =
-  let val curried = Context.exists_name Context.CPureN (Context.theory_of context)
-  in Syntax.pretty_term ext context syn curried t end;
+fun pretty_term' ctxt syn ext t =
+  let val curried = Context.exists_name Context.CPureN (ProofContext.theory_of ctxt)
+  in Syntax.pretty_term ext ctxt syn curried t end;
 
 fun pretty_term thy t =
-  pretty_term' (Context.Theory thy) (syn_of thy) (Consts.extern (consts_of thy))
+  pretty_term' (ProofContext.init thy) (syn_of thy) (Consts.extern (consts_of thy))
     (extern_term (Consts.extern_early (consts_of thy)) thy t);
 
-fun pretty_typ thy T = Syntax.pretty_typ (Context.Theory thy) (syn_of thy) (extern_typ thy T);
-fun pretty_sort thy S = Syntax.pretty_sort (Context.Theory thy) (syn_of thy) (extern_sort thy S);
+fun pretty_typ thy T =
+  Syntax.pretty_typ (ProofContext.init thy) (syn_of thy) (extern_typ thy T);
+
+fun pretty_sort thy S =
+  Syntax.pretty_sort (ProofContext.init thy) (syn_of thy) (extern_sort thy S);
 
 fun pretty_classrel thy cs = Pretty.block (flat
   (separate [Pretty.str " <", Pretty.brk 1] (map (single o pretty_sort thy o single) cs)));
@@ -510,14 +512,14 @@
 fun read_class thy c = certify_class thy (intern_class thy c)
   handle TYPE (msg, _, _) => error msg;
 
-fun read_sort' syn context str =
+fun read_sort' syn ctxt str =
   let
-    val thy = Context.theory_of context;
+    val thy = ProofContext.theory_of ctxt;
     val _ = Context.check_thy thy;
-    val S = intern_sort thy (Syntax.read_sort context syn str);
+    val S = intern_sort thy (Syntax.read_sort ctxt syn str);
   in certify_sort thy S handle TYPE (msg, _, _) => error msg end;
 
-fun read_sort thy str = read_sort' (syn_of thy) (Context.Theory thy) str;
+fun read_sort thy str = read_sort' (syn_of thy) (ProofContext.init thy) str;
 
 
 (* type arities *)
@@ -534,17 +536,17 @@
 
 local
 
-fun gen_read_typ' cert syn context def_sort str =
+fun gen_read_typ' cert syn ctxt def_sort str =
   let
-    val thy = Context.theory_of context;
+    val thy = ProofContext.theory_of ctxt;
     val _ = Context.check_thy thy;
     val get_sort = TypeInfer.get_sort (tsig_of thy) def_sort (intern_sort thy);
-    val T = intern_tycons thy (Syntax.read_typ context syn get_sort (intern_sort thy) str);
+    val T = intern_tycons thy (Syntax.read_typ ctxt syn get_sort (intern_sort thy) str);
   in cert thy T handle TYPE (msg, _, _) => error msg end
   handle ERROR msg => cat_error msg ("The error(s) above occurred in type " ^ quote str);
 
 fun gen_read_typ cert (thy, def_sort) str =
-  gen_read_typ' cert (syn_of thy) (Context.Theory thy) def_sort str;
+  gen_read_typ' cert (syn_of thy) (ProofContext.init thy) def_sort str;
 
 in
 
@@ -620,12 +622,12 @@
 
 (* read_def_terms -- read terms and infer types *)    (*exception ERROR*)
 
-fun read_def_terms' pp is_logtype syn consts context (types, sorts) used freeze sTs =
+fun read_def_terms' pp is_logtype syn consts ctxt (types, sorts) used freeze sTs =
   let
-    val thy = Context.theory_of context;
+    val thy = ProofContext.theory_of ctxt;
     fun read (s, T) =
       let val T' = certify_typ thy T handle TYPE (msg, _, _) => error msg
-      in (Syntax.read context is_logtype syn T' s, T') end;
+      in (Syntax.read ctxt is_logtype syn T' s, T') end;
   in infer_types_simult pp thy consts types sorts used freeze (map read sTs) end;
 
 fun read_def_terms (thy, types, sorts) used freeze sTs =
@@ -635,7 +637,7 @@
     val cert_consts = Consts.certify pp (tsig_of thy) consts;
     val (ts, inst) =
       read_def_terms' pp (is_logtype thy) (syn_of thy) consts
-        (Context.Theory thy) (types, sorts) (Name.make_context used) freeze sTs;
+        (ProofContext.init thy) (types, sorts) (Name.make_context used) freeze sTs;
   in (map cert_consts ts, inst) end;
 
 fun simple_read_term thy T s =
@@ -827,7 +829,7 @@
 local
 
 fun advancedT false = ""
-  | advancedT true = "Context.generic -> ";
+  | advancedT true = "Proof.context -> ";
 
 fun advancedN false = ""
   | advancedN true = "advanced_";
@@ -870,7 +872,7 @@
 
 fun gen_trrules f args thy = thy |> map_syn (fn syn =>
   let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
-  in f (Context.Theory thy) (is_logtype thy) syn rules syn end);
+  in f (ProofContext.init thy) (is_logtype thy) syn rules syn end);
 
 val add_trrules = gen_trrules Syntax.extend_trrules;
 val del_trrules = gen_trrules Syntax.remove_trrules;