advanced translation functions: Proof.context;

--- a/src/HOL/Tools/datatype_package.ML	Mon Dec 11 19:05:25 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML	Mon Dec 11 21:39:26 2006 +0100
@@ -392,9 +392,9 @@
 
 (**** translation rules for case ****)
 
-fun case_tr context [t, u] =
+fun case_tr ctxt [t, u] =
     let
-      val thy = Context.theory_of context;
+      val thy = ProofContext.theory_of ctxt;
       fun case_error s name ts = raise TERM ("Error in case expression" ^
         getOpt (Option.map (curry op ^ " for datatype ") name, "") ^ ":\n" ^ s, ts);
       fun dest_case1 (Const ("_case1", _) $ t $ u) =
@@ -457,10 +457,10 @@
     end
   | case_tr _ ts = raise TERM ("case_tr", ts);
 
-fun case_tr' constrs context ts =
+fun case_tr' constrs ctxt ts =
   if length ts <> length constrs + 1 then raise Match else
   let
-    val consts = Context.cases Sign.consts_of ProofContext.consts_of context;
+    val consts = ProofContext.consts_of ctxt;
 
     val (fs, x) = split_last ts;
     fun strip_abs 0 t = ([], t)

--- a/src/HOL/Tools/record_package.ML	Mon Dec 11 19:05:25 2006 +0100
+++ b/src/HOL/Tools/record_package.ML	Mon Dec 11 21:39:26 2006 +0100
@@ -538,9 +538,9 @@
      else [dest_ext_field mark trm]
   | dest_ext_fields _ mark t = [dest_ext_field mark t]
 
-fun gen_ext_fields_tr sep mark sfx more context t =
+fun gen_ext_fields_tr sep mark sfx more ctxt t =
   let
-    val thy = Context.theory_of context;
+    val thy = ProofContext.theory_of ctxt;
     val msg = "error in record input: ";
     val fieldargs = dest_ext_fields sep mark t;
     fun splitargs (field::fields) ((name,arg)::fargs) =
@@ -568,9 +568,9 @@
 
   in mk_ext fieldargs end;
 
-fun gen_ext_type_tr sep mark sfx more context t =
+fun gen_ext_type_tr sep mark sfx more ctxt t =
   let
-    val thy = Context.theory_of context;
+    val thy = ProofContext.theory_of ctxt;
     val msg = "error in record-type input: ";
     val fieldargs = dest_ext_fields sep mark t;
     fun splitargs (field::fields) ((name,arg)::fargs) =
@@ -619,20 +619,20 @@
 
   in mk_ext fieldargs end;
 
-fun gen_adv_record_tr sep mark sfx unit context [t] =
-      gen_ext_fields_tr sep mark sfx unit context t
+fun gen_adv_record_tr sep mark sfx unit ctxt [t] =
+      gen_ext_fields_tr sep mark sfx unit ctxt t
   | gen_adv_record_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
 
-fun gen_adv_record_scheme_tr sep mark sfx context [t, more] =
-      gen_ext_fields_tr sep mark sfx more context t
+fun gen_adv_record_scheme_tr sep mark sfx ctxt [t, more] =
+      gen_ext_fields_tr sep mark sfx more ctxt t
   | gen_adv_record_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
 
-fun gen_adv_record_type_tr sep mark sfx unit context [t] =
-      gen_ext_type_tr sep mark sfx unit context t
+fun gen_adv_record_type_tr sep mark sfx unit ctxt [t] =
+      gen_ext_type_tr sep mark sfx unit ctxt t
   | gen_adv_record_type_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
 
-fun gen_adv_record_type_scheme_tr sep mark sfx context [t, more] =
-      gen_ext_type_tr sep mark sfx more context t
+fun gen_adv_record_type_scheme_tr sep mark sfx ctxt [t, more] =
+      gen_ext_type_tr sep mark sfx more ctxt t
   | gen_adv_record_type_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
 
 val adv_record_tr = gen_adv_record_tr "_fields" "_field" extN HOLogic.unit;
@@ -680,9 +680,9 @@
   let val name_sfx = suffix sfx name
   in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
 
-fun record_tr' sep mark record record_scheme unit context t =
+fun record_tr' sep mark record record_scheme unit ctxt t =
   let
-    val thy = Context.theory_of context;
+    val thy = ProofContext.theory_of ctxt;
     fun field_lst t =
       (case strip_comb t of
         (Const (ext,_),args as (_::_))
@@ -713,7 +713,7 @@
 fun gen_record_tr' name =
   let val name_sfx = suffix extN name;
       val unit = (fn Const ("Unity",_) => true | _ => false);
-      fun tr' context ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit context
+      fun tr' ctxt ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit ctxt
                        (list_comb (Syntax.const name_sfx,ts))
   in (name_sfx,tr')
   end
@@ -724,9 +724,9 @@
 
 (* record_type_abbr_tr' tries to reconstruct the record name type abbreviation from *)
 (* the (nested) extension types.                                                    *)
-fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT context tm =
+fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt tm =
   let
-      val thy = Context.theory_of context;
+      val thy = ProofContext.theory_of ctxt;
       (* tm is term representation of a (nested) field type. We first reconstruct the      *)
       (* type from tm so that we can continue on the type level rather then the term level.*)
 
@@ -770,15 +770,15 @@
                     if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree(zeta,Sign.defaultS thy))))
                     then mk_type_abbr subst abbr alphas
                     else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta])
-                   end handle TYPE_MATCH => default_tr' context tm)
+                   end handle TYPE_MATCH => default_tr' ctxt tm)
                  else raise Match (* give print translation of specialised record a chance *)
             | _ => raise Match)
-       else default_tr' context tm
+       else default_tr' ctxt tm
   end
 
-fun record_type_tr' sep mark record record_scheme context t =
+fun record_type_tr' sep mark record record_scheme ctxt t =
   let
-    val thy = Context.theory_of context;
+    val thy = ProofContext.theory_of ctxt;
     fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS thy);
 
     val T = Sign.intern_typ thy (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t)
@@ -826,8 +826,8 @@
 
 fun gen_record_type_tr' name =
   let val name_sfx = suffix ext_typeN name;
-      fun tr' context ts = record_type_tr' "_field_types" "_field_type"
-                       "_record_type" "_record_type_scheme" context
+      fun tr' ctxt ts = record_type_tr' "_field_types" "_field_type"
+                       "_record_type" "_record_type_scheme" ctxt
                        (list_comb (Syntax.const name_sfx,ts))
   in (name_sfx,tr')
   end
@@ -837,8 +837,8 @@
   let val name_sfx = suffix ext_typeN name;
       val default_tr' = record_type_tr' "_field_types" "_field_type"
                                "_record_type" "_record_type_scheme"
-      fun tr' context ts =
-          record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT context
+      fun tr' ctxt ts =
+          record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt
                                (list_comb (Syntax.const name_sfx,ts))
   in (name_sfx, tr') end;
 

--- a/src/Pure/Isar/proof_context.ML	Mon Dec 11 19:05:25 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Dec 11 21:39:26 2006 +0100
@@ -293,9 +293,7 @@
       |> do_abbrevs ? rewrite_term false thy (Consts.abbrevs_of consts [#1 Syntax.internal_mode])
       |> Sign.extern_term (Consts.extern_early consts) thy
       |> LocalSyntax.extern_term syntax;
-  in
-    Sign.pretty_term' (Context.Proof ctxt) (LocalSyntax.syn_of syntax) (Consts.extern consts) t'
-  end;
+  in Sign.pretty_term' ctxt (LocalSyntax.syn_of syntax) (Consts.extern consts) t' end;
 
 in
 
@@ -355,7 +353,7 @@
 local
 
 fun read_typ_aux read ctxt s =
-  read (syn_of ctxt) (Context.Proof ctxt) (Variable.def_sort ctxt) s;
+  read (syn_of ctxt) ctxt (Variable.def_sort ctxt) s;
 
 fun cert_typ_aux cert ctxt raw_T =
   cert (theory_of ctxt) raw_T handle TYPE (msg, _, _) => error msg;
@@ -435,7 +433,7 @@
 
 fun read_def_termTs freeze pp syn ctxt (types, sorts, used) sTs =
   Sign.read_def_terms' pp (Sign.is_logtype (theory_of ctxt)) syn (consts_of ctxt)
-    (Context.Proof ctxt) (types, sorts) used freeze sTs;
+    ctxt (types, sorts) used freeze sTs;
 
 fun read_def_termT freeze pp syn ctxt defaults sT =
   apfst hd (read_def_termTs freeze pp syn ctxt defaults [sT]);
@@ -865,9 +863,9 @@
       Option.map (pair false) (try (Consts.syntax (consts_of ctxt)) (c, mx))
   | const_syntax _ _ = NONE;
 
-fun context_const_ast_tr context [Syntax.Variable c] =
+fun context_const_ast_tr ctxt [Syntax.Variable c] =
       let
-        val consts = Context.cases Sign.consts_of consts_of context;
+        val consts = consts_of ctxt;
         val c' = Consts.intern consts c;
         val _ = Consts.the_constraint consts c' handle TYPE (msg, _, _) => error msg;
       in Syntax.Constant (Syntax.constN ^ c') end

--- a/src/Pure/Syntax/printer.ML	Mon Dec 11 19:05:25 2006 +0100
+++ b/src/Pure/Syntax/printer.ML	Mon Dec 11 21:39:26 2006 +0100
@@ -18,22 +18,22 @@
 signature PRINTER =
 sig
   include PRINTER0
-  val term_to_ast: Context.generic ->
-    (string -> (Context.generic -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
-  val typ_to_ast: Context.generic ->
-    (string -> (Context.generic -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast
-  val sort_to_ast: Context.generic ->
-    (string -> (Context.generic -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
+  val term_to_ast: Proof.context ->
+    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
+  val typ_to_ast: Proof.context ->
+    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast
+  val sort_to_ast: Proof.context ->
+    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
   type prtabs
   val empty_prtabs: prtabs
   val extend_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
   val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
   val merge_prtabs: prtabs -> prtabs -> prtabs
-  val pretty_term_ast: (string -> xstring) -> Context.generic -> bool -> prtabs
-    -> (string -> (Context.generic -> Ast.ast list -> Ast.ast) list)
+  val pretty_term_ast: (string -> xstring) -> Proof.context -> bool -> prtabs
+    -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
     -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T
-  val pretty_typ_ast: Context.generic -> bool -> prtabs
-    -> (string -> (Context.generic -> Ast.ast list -> Ast.ast) list)
+  val pretty_typ_ast: Proof.context -> bool -> prtabs
+    -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
     -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T
 end;
 
@@ -58,17 +58,17 @@
 
 (* apply print (ast) translation function *)
 
-fun apply_trans context name a fns args =
+fun apply_trans ctxt name a fns args =
   let
     fun app_first [] = raise Match
-      | app_first (f :: fs) = f context args handle Match => app_first fs;
+      | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
   in
     transform_failure (fn Match => Match
       | exn => EXCEPTION (exn, "Error in " ^ name ^ " for " ^ quote a))
       app_first fns
   end;
 
-fun apply_typed x y fs = map (fn f => fn context => f context x y) fs;
+fun apply_typed x y fs = map (fn f => fn ctxt => f ctxt x y) fs;
 
 
 (* simple_ast_of *)
@@ -87,7 +87,7 @@
 
 (** sort_to_ast, typ_to_ast **)
 
-fun ast_of_termT context trf tm =
+fun ast_of_termT ctxt trf tm =
   let
     fun ast_of (t as Const ("_class", _) $ Free _) = simple_ast_of t
       | ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
@@ -99,12 +99,12 @@
           | (f, args) => Ast.Appl (map ast_of (f :: args)))
       | ast_of t = simple_ast_of t
     and trans a args =
-      ast_of (apply_trans context "print translation" a (apply_typed false dummyT (trf a)) args)
+      ast_of (apply_trans ctxt "print translation" a (apply_typed false dummyT (trf a)) args)
         handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
   in ast_of tm end;
 
-fun sort_to_ast context trf S = ast_of_termT context trf (TypeExt.term_of_sort S);
-fun typ_to_ast context trf T = ast_of_termT context trf (TypeExt.term_of_typ (! show_sorts) T);
+fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (TypeExt.term_of_sort S);
+fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (TypeExt.term_of_typ (! show_sorts) T);
 
 
 
@@ -121,7 +121,7 @@
       else Lexicon.const "_var" $ t
   | mark_freevars a = a;
 
-fun ast_of_term context trf show_all_types no_freeTs show_types show_sorts tm =
+fun ast_of_term ctxt trf show_all_types no_freeTs show_types show_sorts tm =
   let
     fun prune_typs (t_seen as (Const _, _)) = t_seen
       | prune_typs (t as Free (x, ty), seen) =
@@ -160,13 +160,13 @@
       | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
 
     and trans a T args =
-      ast_of (apply_trans context "print translation" a (apply_typed show_sorts T (trf a)) args)
+      ast_of (apply_trans ctxt "print translation" a (apply_typed show_sorts T (trf a)) args)
         handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
 
     and constrain t T =
       if show_types andalso T <> dummyT then
         Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t,
-          ast_of_termT context trf (TypeExt.term_of_typ show_sorts T)]
+          ast_of_termT ctxt trf (TypeExt.term_of_typ show_sorts T)]
       else simple_ast_of t
   in
     tm
@@ -176,8 +176,8 @@
     |> ast_of
   end;
 
-fun term_to_ast context trf tm =
-  ast_of_term context trf (! show_all_types) (! show_no_free_types)
+fun term_to_ast ctxt trf tm =
+  ast_of_term ctxt trf (! show_all_types) (! show_no_free_types)
     (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) tm;
 
 
@@ -267,9 +267,9 @@
   | is_chain [Arg _] = true
   | is_chain _  = false;
 
-fun pretty extern_const context tabs trf tokentrf type_mode curried ast0 p0 =
+fun pretty extern_const ctxt tabs trf tokentrf type_mode curried ast0 p0 =
   let
-    val trans = apply_trans context "print ast translation";
+    val trans = apply_trans ctxt "print ast translation";
 
     fun token_trans c [Ast.Variable x] =
           (case tokentrf c of
@@ -292,7 +292,7 @@
             val (Ts, args') = synT (symbs, args);
           in
             if type_mode then (astT (t, p) @ Ts, args')
-            else (pretty I context tabs trf tokentrf true curried t p @ Ts, args')
+            else (pretty I ctxt tabs trf tokentrf true curried t p @ Ts, args')
           end
       | synT (String s :: symbs, args) =
           let val (Ts, args') = synT (symbs, args);
@@ -366,15 +366,15 @@
 
 (* pretty_term_ast *)
 
-fun pretty_term_ast extern_const context curried prtabs trf tokentrf ast =
-  Pretty.blk (0, pretty extern_const context (mode_tabs prtabs (! print_mode))
+fun pretty_term_ast extern_const ctxt curried prtabs trf tokentrf ast =
+  Pretty.blk (0, pretty extern_const ctxt (mode_tabs prtabs (! print_mode))
     trf tokentrf false curried ast 0);
 
 
 (* pretty_typ_ast *)
 
-fun pretty_typ_ast context _ prtabs trf tokentrf ast =
-  Pretty.blk (0, pretty I context (mode_tabs prtabs (! print_mode))
+fun pretty_typ_ast ctxt _ prtabs trf tokentrf ast =
+  Pretty.blk (0, pretty I ctxt (mode_tabs prtabs (! print_mode))
     trf tokentrf true false ast 0);
 
 end;

--- a/src/Pure/Syntax/syn_ext.ML	Mon Dec 11 19:05:25 2006 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Mon Dec 11 21:39:26 2006 +0100
@@ -42,33 +42,30 @@
       xprods: xprod list,
       consts: string list,
       prmodes: string list,
-      parse_ast_translation:
-        (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
+      parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
       parse_rules: (Ast.ast * Ast.ast) list,
-      parse_translation:
-        (string * ((Context.generic -> term list -> term) * stamp)) list,
+      parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
       print_translation:
-        (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list,
+        (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
       print_rules: (Ast.ast * Ast.ast) list,
-      print_ast_translation:
-        (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
+      print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
       token_translation: (string * string * (string -> string * real)) list}
   val mfix_delims: string -> string list
   val mfix_args: string -> int
   val escape_mfix: string -> string
   val unlocalize_mfix: string -> string
   val syn_ext': bool -> (string -> bool) -> mfix list ->
-    string list -> (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list *
-    (string * ((Context.generic -> term list -> term) * stamp)) list *
-    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
-    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list
+    string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
+    (string * ((Proof.context -> term list -> term) * stamp)) list *
+    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
+    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
     -> (string * string * (string -> string * real)) list
     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   val syn_ext: mfix list -> string list ->
-    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list *
-    (string * ((Context.generic -> term list -> term) * stamp)) list *
-    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
-    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list
+    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
+    (string * ((Proof.context -> term list -> term) * stamp)) list *
+    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
+    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
     -> (string * string * (string -> string * real)) list
     -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   val syn_ext_const_names: string list -> syn_ext
@@ -79,10 +76,10 @@
     (string * ((bool -> typ -> term list -> term) * stamp)) list *
     (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
   val syn_ext_advanced_trfuns:
-    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list *
-    (string * ((Context.generic -> term list -> term) * stamp)) list *
-    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
-    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
+    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
+    (string * ((Proof.context -> term list -> term) * stamp)) list *
+    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
+    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
   val syn_ext_tokentrfuns: (string * string * (string -> string * real)) list -> syn_ext
   val standard_token_markers: string list
   val pure_ext: syn_ext
@@ -339,16 +336,13 @@
     xprods: xprod list,
     consts: string list,
     prmodes: string list,
-    parse_ast_translation:
-      (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
+    parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
     parse_rules: (Ast.ast * Ast.ast) list,
-    parse_translation:
-      (string * ((Context.generic -> term list -> term) * stamp)) list,
+    parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
     print_translation:
-      (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list,
+      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
     print_rules: (Ast.ast * Ast.ast) list,
-    print_ast_translation:
-      (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
+    print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
     token_translation: (string * string * (string -> string * real)) list};
 
 

--- a/src/Pure/Syntax/syntax.ML	Mon Dec 11 19:05:25 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML	Mon Dec 11 21:39:26 2006 +0100
@@ -51,16 +51,16 @@
     (string * ((bool -> typ -> term list -> term) * stamp)) list *
     (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax
   val extend_advanced_trfuns:
-    (string * ((Context.generic -> ast list -> ast) * stamp)) list *
-    (string * ((Context.generic -> term list -> term) * stamp)) list *
-    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
-    (string * ((Context.generic -> ast list -> ast) * stamp)) list -> syntax -> syntax
+    (string * ((Proof.context -> ast list -> ast) * stamp)) list *
+    (string * ((Proof.context -> term list -> term) * stamp)) list *
+    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
+    (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
   val extend_tokentrfuns: (string * string * (string -> string * real)) list -> syntax -> syntax
   val remove_const_gram: (string -> bool) ->
     mode -> (string * typ * mixfix) list -> syntax -> syntax
-  val extend_trrules: Context.generic -> (string -> bool) -> syntax ->
+  val extend_trrules: Proof.context -> (string -> bool) -> syntax ->
     (string * string) trrule list -> syntax -> syntax
-  val remove_trrules: Context.generic -> (string -> bool) -> syntax ->
+  val remove_trrules: Proof.context -> (string -> bool) -> syntax ->
     (string * string) trrule list -> syntax -> syntax
   val extend_trrules_i: ast trrule list -> syntax -> syntax
   val remove_trrules_i: ast trrule list -> syntax -> syntax
@@ -73,13 +73,13 @@
   val print_gram: syntax -> unit
   val print_trans: syntax -> unit
   val print_syntax: syntax -> unit
-  val read: Context.generic -> (string -> bool) -> syntax -> typ -> string -> term list
-  val read_typ: Context.generic -> syntax -> ((indexname * sort) list -> indexname -> sort) ->
+  val read: Proof.context -> (string -> bool) -> syntax -> typ -> string -> term list
+  val read_typ: Proof.context -> syntax -> ((indexname * sort) list -> indexname -> sort) ->
     (sort -> sort) -> string -> typ
-  val read_sort: Context.generic -> syntax -> string -> sort
-  val pretty_term: (string -> xstring) -> Context.generic -> syntax -> bool -> term -> Pretty.T
-  val pretty_typ: Context.generic -> syntax -> typ -> Pretty.T
-  val pretty_sort: Context.generic -> syntax -> sort -> Pretty.T
+  val read_sort: Proof.context -> syntax -> string -> sort
+  val pretty_term: (string -> xstring) -> Proof.context -> syntax -> bool -> term -> Pretty.T
+  val pretty_typ: Proof.context -> syntax -> typ -> Pretty.T
+  val pretty_sort: Proof.context -> syntax -> sort -> Pretty.T
   val ambiguity_level: int ref
   val ambiguity_is_error: bool ref
 end;
@@ -172,12 +172,12 @@
     gram: Parser.gram,
     consts: string list,
     prmodes: string list,
-    parse_ast_trtab: ((Context.generic -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
+    parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
     parse_ruletab: ruletab,
-    parse_trtab: ((Context.generic -> term list -> term) * stamp) Symtab.table,
-    print_trtab: ((Context.generic -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
+    parse_trtab: ((Proof.context -> term list -> term) * stamp) Symtab.table,
+    print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
     print_ruletab: ruletab,
-    print_ast_trtab: ((Context.generic -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
+    print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
     tokentrtab: (string * (string * ((string -> string * real) * stamp)) list) list,
     prtabs: Printer.prtabs} * stamp;
 
@@ -384,7 +384,7 @@
 val ambiguity_level = ref 1;
 val ambiguity_is_error = ref false
 
-fun read_asts context is_logtype (Syntax (tabs, _)) xids root str =
+fun read_asts ctxt is_logtype (Syntax (tabs, _)) xids root str =
   let
     val {lexicon, gram, parse_ast_trtab, ...} = tabs;
     val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
@@ -392,41 +392,41 @@
     val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
 
     fun show_pt pt =
-      Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts context (K NONE) [pt])));
+      Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts ctxt (K NONE) [pt])));
   in
     conditional (length pts > ! ambiguity_level) (fn () =>
       if ! ambiguity_is_error then error ("Ambiguous input " ^ quote str)
       else (warning ("Ambiguous input " ^ quote str ^ "\n" ^
           "produces " ^ string_of_int (length pts) ^ " parse trees.");
          List.app (warning o show_pt) pts));
-    SynTrans.pts_to_asts context (lookup_tr parse_ast_trtab) pts
+    SynTrans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
   end;
 
 
 (* read *)
 
-fun read context is_logtype (syn as Syntax (tabs, _)) ty str =
+fun read ctxt is_logtype (syn as Syntax (tabs, _)) ty str =
   let
     val {parse_ruletab, parse_trtab, ...} = tabs;
-    val asts = read_asts context is_logtype syn false (SynExt.typ_to_nonterm ty) str;
+    val asts = read_asts ctxt is_logtype syn false (SynExt.typ_to_nonterm ty) str;
   in
-    SynTrans.asts_to_terms context (lookup_tr parse_trtab)
+    SynTrans.asts_to_terms ctxt (lookup_tr parse_trtab)
       (map (Ast.normalize_ast (Symtab.lookup_list parse_ruletab)) asts)
   end;
 
 
 (* read types *)
 
-fun read_typ context syn get_sort map_sort str =
-  (case read context (K false) syn SynExt.typeT str of
+fun read_typ ctxt syn get_sort map_sort str =
+  (case read ctxt (K false) syn SynExt.typeT str of
     [t] => TypeExt.typ_of_term (get_sort (TypeExt.raw_term_sorts t)) map_sort t
   | _ => error "read_typ: ambiguous syntax");
 
 
 (* read sorts *)
 
-fun read_sort context syn str =
-  (case read context (K false) syn TypeExt.sortT str of
+fun read_sort ctxt syn str =
+  (case read ctxt (K false) syn TypeExt.sortT str of
     [t] => TypeExt.sort_of_term t
   | _ => error "read_sort: ambiguous syntax");
 
@@ -462,7 +462,7 @@
   | NONE => rule);
 
 
-fun read_pattern context is_logtype syn (root, str) =
+fun read_pattern ctxt is_logtype syn (root, str) =
   let
     val Syntax ({consts, ...}, _) = syn;
 
@@ -472,7 +472,7 @@
           else ast
       | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
   in
-    (case read_asts context is_logtype syn true root str of
+    (case read_asts ctxt is_logtype syn true root str of
       [ast] => constify ast
     | _ => error ("Syntactically ambiguous input: " ^ quote str))
   end handle ERROR msg =>
@@ -489,8 +489,8 @@
 
 val cert_rules = prep_rules I;
 
-fun read_rules context is_logtype syn =
-  prep_rules (read_pattern context is_logtype syn);
+fun read_rules ctxt is_logtype syn =
+  prep_rules (read_pattern ctxt is_logtype syn);
 
 end;
 
@@ -498,19 +498,19 @@
 
 (** pretty terms, typs, sorts **)
 
-fun pretty_t t_to_ast prt_t context (syn as Syntax (tabs, _)) curried t =
+fun pretty_t t_to_ast prt_t ctxt (syn as Syntax (tabs, _)) curried t =
   let
     val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
-    val ast = t_to_ast context (lookup_tr' print_trtab) t;
+    val ast = t_to_ast ctxt (lookup_tr' print_trtab) t;
   in
-    prt_t context curried prtabs (lookup_tr' print_ast_trtab)
+    prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
       (lookup_tokentr tokentrtab (! print_mode))
       (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast)
   end;
 
 val pretty_term = pretty_t Printer.term_to_ast o Printer.pretty_term_ast;
-fun pretty_typ context syn = pretty_t Printer.typ_to_ast Printer.pretty_typ_ast context syn false;
-fun pretty_sort context syn = pretty_t Printer.sort_to_ast Printer.pretty_typ_ast context syn false;
+fun pretty_typ ctxt syn = pretty_t Printer.typ_to_ast Printer.pretty_typ_ast ctxt syn false;
+fun pretty_sort ctxt syn = pretty_t Printer.sort_to_ast Printer.pretty_typ_ast ctxt syn false;
 
 
 
@@ -529,11 +529,11 @@
 fun remove_const_gram is_logtype prmode decls =
   remove_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);
 
-fun extend_trrules context is_logtype syn =
-  ext_syntax SynExt.syn_ext_rules o read_rules context is_logtype syn;
+fun extend_trrules ctxt is_logtype syn =
+  ext_syntax SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
 
-fun remove_trrules context is_logtype syn =
-  remove_syntax default_mode o SynExt.syn_ext_rules o read_rules context is_logtype syn;
+fun remove_trrules ctxt is_logtype syn =
+  remove_syntax default_mode o SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
 
 val extend_trrules_i = ext_syntax SynExt.syn_ext_rules o cert_rules;
 val remove_trrules_i = remove_syntax default_mode o SynExt.syn_ext_rules o cert_rules;

--- 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;

--- a/src/Pure/theory.ML	Mon Dec 11 19:05:25 2006 +0100
+++ b/src/Pure/theory.ML	Mon Dec 11 21:39:26 2006 +0100
@@ -178,7 +178,7 @@
 
 fun read_def_axm (thy, types, sorts) used (name, str) =
   let
-    val ts = Syntax.read (Context.Theory thy) (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
+    val ts = Syntax.read (ProofContext.init thy) (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
     val (t, _) =
       Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy)
         types sorts (Name.make_context used) true (ts, propT);