advanced translation functions: Proof.context;
authorwenzelm
Mon Dec 11 21:39:26 2006 +0100 (2006-12-11)
changeset 217727c7ade4f537b
parent 21771 148c8aba89dd
child 21773 0038f5fc2065
advanced translation functions: Proof.context;
src/HOL/Tools/datatype_package.ML
src/HOL/Tools/record_package.ML
src/Pure/Isar/proof_context.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syn_ext.ML
src/Pure/Syntax/syntax.ML
src/Pure/sign.ML
src/Pure/theory.ML
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Mon Dec 11 19:05:25 2006 +0100
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Mon Dec 11 21:39:26 2006 +0100
     1.3 @@ -392,9 +392,9 @@
     1.4  
     1.5  (**** translation rules for case ****)
     1.6  
     1.7 -fun case_tr context [t, u] =
     1.8 +fun case_tr ctxt [t, u] =
     1.9      let
    1.10 -      val thy = Context.theory_of context;
    1.11 +      val thy = ProofContext.theory_of ctxt;
    1.12        fun case_error s name ts = raise TERM ("Error in case expression" ^
    1.13          getOpt (Option.map (curry op ^ " for datatype ") name, "") ^ ":\n" ^ s, ts);
    1.14        fun dest_case1 (Const ("_case1", _) $ t $ u) =
    1.15 @@ -457,10 +457,10 @@
    1.16      end
    1.17    | case_tr _ ts = raise TERM ("case_tr", ts);
    1.18  
    1.19 -fun case_tr' constrs context ts =
    1.20 +fun case_tr' constrs ctxt ts =
    1.21    if length ts <> length constrs + 1 then raise Match else
    1.22    let
    1.23 -    val consts = Context.cases Sign.consts_of ProofContext.consts_of context;
    1.24 +    val consts = ProofContext.consts_of ctxt;
    1.25  
    1.26      val (fs, x) = split_last ts;
    1.27      fun strip_abs 0 t = ([], t)
     2.1 --- a/src/HOL/Tools/record_package.ML	Mon Dec 11 19:05:25 2006 +0100
     2.2 +++ b/src/HOL/Tools/record_package.ML	Mon Dec 11 21:39:26 2006 +0100
     2.3 @@ -538,9 +538,9 @@
     2.4       else [dest_ext_field mark trm]
     2.5    | dest_ext_fields _ mark t = [dest_ext_field mark t]
     2.6  
     2.7 -fun gen_ext_fields_tr sep mark sfx more context t =
     2.8 +fun gen_ext_fields_tr sep mark sfx more ctxt t =
     2.9    let
    2.10 -    val thy = Context.theory_of context;
    2.11 +    val thy = ProofContext.theory_of ctxt;
    2.12      val msg = "error in record input: ";
    2.13      val fieldargs = dest_ext_fields sep mark t;
    2.14      fun splitargs (field::fields) ((name,arg)::fargs) =
    2.15 @@ -568,9 +568,9 @@
    2.16  
    2.17    in mk_ext fieldargs end;
    2.18  
    2.19 -fun gen_ext_type_tr sep mark sfx more context t =
    2.20 +fun gen_ext_type_tr sep mark sfx more ctxt t =
    2.21    let
    2.22 -    val thy = Context.theory_of context;
    2.23 +    val thy = ProofContext.theory_of ctxt;
    2.24      val msg = "error in record-type input: ";
    2.25      val fieldargs = dest_ext_fields sep mark t;
    2.26      fun splitargs (field::fields) ((name,arg)::fargs) =
    2.27 @@ -619,20 +619,20 @@
    2.28  
    2.29    in mk_ext fieldargs end;
    2.30  
    2.31 -fun gen_adv_record_tr sep mark sfx unit context [t] =
    2.32 -      gen_ext_fields_tr sep mark sfx unit context t
    2.33 +fun gen_adv_record_tr sep mark sfx unit ctxt [t] =
    2.34 +      gen_ext_fields_tr sep mark sfx unit ctxt t
    2.35    | gen_adv_record_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
    2.36  
    2.37 -fun gen_adv_record_scheme_tr sep mark sfx context [t, more] =
    2.38 -      gen_ext_fields_tr sep mark sfx more context t
    2.39 +fun gen_adv_record_scheme_tr sep mark sfx ctxt [t, more] =
    2.40 +      gen_ext_fields_tr sep mark sfx more ctxt t
    2.41    | gen_adv_record_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
    2.42  
    2.43 -fun gen_adv_record_type_tr sep mark sfx unit context [t] =
    2.44 -      gen_ext_type_tr sep mark sfx unit context t
    2.45 +fun gen_adv_record_type_tr sep mark sfx unit ctxt [t] =
    2.46 +      gen_ext_type_tr sep mark sfx unit ctxt t
    2.47    | gen_adv_record_type_tr _ _ _ _ _ ts = raise TERM ("gen_record_tr", ts);
    2.48  
    2.49 -fun gen_adv_record_type_scheme_tr sep mark sfx context [t, more] =
    2.50 -      gen_ext_type_tr sep mark sfx more context t
    2.51 +fun gen_adv_record_type_scheme_tr sep mark sfx ctxt [t, more] =
    2.52 +      gen_ext_type_tr sep mark sfx more ctxt t
    2.53    | gen_adv_record_type_scheme_tr _ _ _ _ ts = raise TERM ("gen_record_scheme_tr", ts);
    2.54  
    2.55  val adv_record_tr = gen_adv_record_tr "_fields" "_field" extN HOLogic.unit;
    2.56 @@ -680,9 +680,9 @@
    2.57    let val name_sfx = suffix sfx name
    2.58    in (name_sfx, fn [t, u] => tr' (Syntax.const name_sfx $ t $ u) | _ => raise Match) end;
    2.59  
    2.60 -fun record_tr' sep mark record record_scheme unit context t =
    2.61 +fun record_tr' sep mark record record_scheme unit ctxt t =
    2.62    let
    2.63 -    val thy = Context.theory_of context;
    2.64 +    val thy = ProofContext.theory_of ctxt;
    2.65      fun field_lst t =
    2.66        (case strip_comb t of
    2.67          (Const (ext,_),args as (_::_))
    2.68 @@ -713,7 +713,7 @@
    2.69  fun gen_record_tr' name =
    2.70    let val name_sfx = suffix extN name;
    2.71        val unit = (fn Const ("Unity",_) => true | _ => false);
    2.72 -      fun tr' context ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit context
    2.73 +      fun tr' ctxt ts = record_tr' "_fields" "_field" "_record" "_record_scheme" unit ctxt
    2.74                         (list_comb (Syntax.const name_sfx,ts))
    2.75    in (name_sfx,tr')
    2.76    end
    2.77 @@ -724,9 +724,9 @@
    2.78  
    2.79  (* record_type_abbr_tr' tries to reconstruct the record name type abbreviation from *)
    2.80  (* the (nested) extension types.                                                    *)
    2.81 -fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT context tm =
    2.82 +fun record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt tm =
    2.83    let
    2.84 -      val thy = Context.theory_of context;
    2.85 +      val thy = ProofContext.theory_of ctxt;
    2.86        (* tm is term representation of a (nested) field type. We first reconstruct the      *)
    2.87        (* type from tm so that we can continue on the type level rather then the term level.*)
    2.88  
    2.89 @@ -770,15 +770,15 @@
    2.90                      if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree(zeta,Sign.defaultS thy))))
    2.91                      then mk_type_abbr subst abbr alphas
    2.92                      else mk_type_abbr subst (suffix schemeN abbr) (alphas@[zeta])
    2.93 -                   end handle TYPE_MATCH => default_tr' context tm)
    2.94 +                   end handle TYPE_MATCH => default_tr' ctxt tm)
    2.95                   else raise Match (* give print translation of specialised record a chance *)
    2.96              | _ => raise Match)
    2.97 -       else default_tr' context tm
    2.98 +       else default_tr' ctxt tm
    2.99    end
   2.100  
   2.101 -fun record_type_tr' sep mark record record_scheme context t =
   2.102 +fun record_type_tr' sep mark record record_scheme ctxt t =
   2.103    let
   2.104 -    val thy = Context.theory_of context;
   2.105 +    val thy = ProofContext.theory_of ctxt;
   2.106      fun get_sort xs n = AList.lookup (op =) xs n |> the_default (Sign.defaultS thy);
   2.107  
   2.108      val T = Sign.intern_typ thy (Syntax.typ_of_term (get_sort (Syntax.raw_term_sorts t)) I t)
   2.109 @@ -826,8 +826,8 @@
   2.110  
   2.111  fun gen_record_type_tr' name =
   2.112    let val name_sfx = suffix ext_typeN name;
   2.113 -      fun tr' context ts = record_type_tr' "_field_types" "_field_type"
   2.114 -                       "_record_type" "_record_type_scheme" context
   2.115 +      fun tr' ctxt ts = record_type_tr' "_field_types" "_field_type"
   2.116 +                       "_record_type" "_record_type_scheme" ctxt
   2.117                         (list_comb (Syntax.const name_sfx,ts))
   2.118    in (name_sfx,tr')
   2.119    end
   2.120 @@ -837,8 +837,8 @@
   2.121    let val name_sfx = suffix ext_typeN name;
   2.122        val default_tr' = record_type_tr' "_field_types" "_field_type"
   2.123                                 "_record_type" "_record_type_scheme"
   2.124 -      fun tr' context ts =
   2.125 -          record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT context
   2.126 +      fun tr' ctxt ts =
   2.127 +          record_type_abbr_tr' default_tr' abbr alphas zeta lastExt schemeT ctxt
   2.128                                 (list_comb (Syntax.const name_sfx,ts))
   2.129    in (name_sfx, tr') end;
   2.130  
     3.1 --- a/src/Pure/Isar/proof_context.ML	Mon Dec 11 19:05:25 2006 +0100
     3.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Dec 11 21:39:26 2006 +0100
     3.3 @@ -293,9 +293,7 @@
     3.4        |> do_abbrevs ? rewrite_term false thy (Consts.abbrevs_of consts [#1 Syntax.internal_mode])
     3.5        |> Sign.extern_term (Consts.extern_early consts) thy
     3.6        |> LocalSyntax.extern_term syntax;
     3.7 -  in
     3.8 -    Sign.pretty_term' (Context.Proof ctxt) (LocalSyntax.syn_of syntax) (Consts.extern consts) t'
     3.9 -  end;
    3.10 +  in Sign.pretty_term' ctxt (LocalSyntax.syn_of syntax) (Consts.extern consts) t' end;
    3.11  
    3.12  in
    3.13  
    3.14 @@ -355,7 +353,7 @@
    3.15  local
    3.16  
    3.17  fun read_typ_aux read ctxt s =
    3.18 -  read (syn_of ctxt) (Context.Proof ctxt) (Variable.def_sort ctxt) s;
    3.19 +  read (syn_of ctxt) ctxt (Variable.def_sort ctxt) s;
    3.20  
    3.21  fun cert_typ_aux cert ctxt raw_T =
    3.22    cert (theory_of ctxt) raw_T handle TYPE (msg, _, _) => error msg;
    3.23 @@ -435,7 +433,7 @@
    3.24  
    3.25  fun read_def_termTs freeze pp syn ctxt (types, sorts, used) sTs =
    3.26    Sign.read_def_terms' pp (Sign.is_logtype (theory_of ctxt)) syn (consts_of ctxt)
    3.27 -    (Context.Proof ctxt) (types, sorts) used freeze sTs;
    3.28 +    ctxt (types, sorts) used freeze sTs;
    3.29  
    3.30  fun read_def_termT freeze pp syn ctxt defaults sT =
    3.31    apfst hd (read_def_termTs freeze pp syn ctxt defaults [sT]);
    3.32 @@ -865,9 +863,9 @@
    3.33        Option.map (pair false) (try (Consts.syntax (consts_of ctxt)) (c, mx))
    3.34    | const_syntax _ _ = NONE;
    3.35  
    3.36 -fun context_const_ast_tr context [Syntax.Variable c] =
    3.37 +fun context_const_ast_tr ctxt [Syntax.Variable c] =
    3.38        let
    3.39 -        val consts = Context.cases Sign.consts_of consts_of context;
    3.40 +        val consts = consts_of ctxt;
    3.41          val c' = Consts.intern consts c;
    3.42          val _ = Consts.the_constraint consts c' handle TYPE (msg, _, _) => error msg;
    3.43        in Syntax.Constant (Syntax.constN ^ c') end
     4.1 --- a/src/Pure/Syntax/printer.ML	Mon Dec 11 19:05:25 2006 +0100
     4.2 +++ b/src/Pure/Syntax/printer.ML	Mon Dec 11 21:39:26 2006 +0100
     4.3 @@ -18,22 +18,22 @@
     4.4  signature PRINTER =
     4.5  sig
     4.6    include PRINTER0
     4.7 -  val term_to_ast: Context.generic ->
     4.8 -    (string -> (Context.generic -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
     4.9 -  val typ_to_ast: Context.generic ->
    4.10 -    (string -> (Context.generic -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast
    4.11 -  val sort_to_ast: Context.generic ->
    4.12 -    (string -> (Context.generic -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
    4.13 +  val term_to_ast: Proof.context ->
    4.14 +    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> term -> Ast.ast
    4.15 +  val typ_to_ast: Proof.context ->
    4.16 +    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> typ -> Ast.ast
    4.17 +  val sort_to_ast: Proof.context ->
    4.18 +    (string -> (Proof.context -> bool -> typ -> term list -> term) list) -> sort -> Ast.ast
    4.19    type prtabs
    4.20    val empty_prtabs: prtabs
    4.21    val extend_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
    4.22    val remove_prtabs: string -> SynExt.xprod list -> prtabs -> prtabs
    4.23    val merge_prtabs: prtabs -> prtabs -> prtabs
    4.24 -  val pretty_term_ast: (string -> xstring) -> Context.generic -> bool -> prtabs
    4.25 -    -> (string -> (Context.generic -> Ast.ast list -> Ast.ast) list)
    4.26 +  val pretty_term_ast: (string -> xstring) -> Proof.context -> bool -> prtabs
    4.27 +    -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
    4.28      -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T
    4.29 -  val pretty_typ_ast: Context.generic -> bool -> prtabs
    4.30 -    -> (string -> (Context.generic -> Ast.ast list -> Ast.ast) list)
    4.31 +  val pretty_typ_ast: Proof.context -> bool -> prtabs
    4.32 +    -> (string -> (Proof.context -> Ast.ast list -> Ast.ast) list)
    4.33      -> (string -> (string -> string * real) option) -> Ast.ast -> Pretty.T
    4.34  end;
    4.35  
    4.36 @@ -58,17 +58,17 @@
    4.37  
    4.38  (* apply print (ast) translation function *)
    4.39  
    4.40 -fun apply_trans context name a fns args =
    4.41 +fun apply_trans ctxt name a fns args =
    4.42    let
    4.43      fun app_first [] = raise Match
    4.44 -      | app_first (f :: fs) = f context args handle Match => app_first fs;
    4.45 +      | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
    4.46    in
    4.47      transform_failure (fn Match => Match
    4.48        | exn => EXCEPTION (exn, "Error in " ^ name ^ " for " ^ quote a))
    4.49        app_first fns
    4.50    end;
    4.51  
    4.52 -fun apply_typed x y fs = map (fn f => fn context => f context x y) fs;
    4.53 +fun apply_typed x y fs = map (fn f => fn ctxt => f ctxt x y) fs;
    4.54  
    4.55  
    4.56  (* simple_ast_of *)
    4.57 @@ -87,7 +87,7 @@
    4.58  
    4.59  (** sort_to_ast, typ_to_ast **)
    4.60  
    4.61 -fun ast_of_termT context trf tm =
    4.62 +fun ast_of_termT ctxt trf tm =
    4.63    let
    4.64      fun ast_of (t as Const ("_class", _) $ Free _) = simple_ast_of t
    4.65        | ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
    4.66 @@ -99,12 +99,12 @@
    4.67            | (f, args) => Ast.Appl (map ast_of (f :: args)))
    4.68        | ast_of t = simple_ast_of t
    4.69      and trans a args =
    4.70 -      ast_of (apply_trans context "print translation" a (apply_typed false dummyT (trf a)) args)
    4.71 +      ast_of (apply_trans ctxt "print translation" a (apply_typed false dummyT (trf a)) args)
    4.72          handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
    4.73    in ast_of tm end;
    4.74  
    4.75 -fun sort_to_ast context trf S = ast_of_termT context trf (TypeExt.term_of_sort S);
    4.76 -fun typ_to_ast context trf T = ast_of_termT context trf (TypeExt.term_of_typ (! show_sorts) T);
    4.77 +fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (TypeExt.term_of_sort S);
    4.78 +fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (TypeExt.term_of_typ (! show_sorts) T);
    4.79  
    4.80  
    4.81  
    4.82 @@ -121,7 +121,7 @@
    4.83        else Lexicon.const "_var" $ t
    4.84    | mark_freevars a = a;
    4.85  
    4.86 -fun ast_of_term context trf show_all_types no_freeTs show_types show_sorts tm =
    4.87 +fun ast_of_term ctxt trf show_all_types no_freeTs show_types show_sorts tm =
    4.88    let
    4.89      fun prune_typs (t_seen as (Const _, _)) = t_seen
    4.90        | prune_typs (t as Free (x, ty), seen) =
    4.91 @@ -160,13 +160,13 @@
    4.92        | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
    4.93  
    4.94      and trans a T args =
    4.95 -      ast_of (apply_trans context "print translation" a (apply_typed show_sorts T (trf a)) args)
    4.96 +      ast_of (apply_trans ctxt "print translation" a (apply_typed show_sorts T (trf a)) args)
    4.97          handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
    4.98  
    4.99      and constrain t T =
   4.100        if show_types andalso T <> dummyT then
   4.101          Ast.Appl [Ast.Constant SynExt.constrainC, simple_ast_of t,
   4.102 -          ast_of_termT context trf (TypeExt.term_of_typ show_sorts T)]
   4.103 +          ast_of_termT ctxt trf (TypeExt.term_of_typ show_sorts T)]
   4.104        else simple_ast_of t
   4.105    in
   4.106      tm
   4.107 @@ -176,8 +176,8 @@
   4.108      |> ast_of
   4.109    end;
   4.110  
   4.111 -fun term_to_ast context trf tm =
   4.112 -  ast_of_term context trf (! show_all_types) (! show_no_free_types)
   4.113 +fun term_to_ast ctxt trf tm =
   4.114 +  ast_of_term ctxt trf (! show_all_types) (! show_no_free_types)
   4.115      (! show_types orelse ! show_sorts orelse ! show_all_types) (! show_sorts) tm;
   4.116  
   4.117  
   4.118 @@ -267,9 +267,9 @@
   4.119    | is_chain [Arg _] = true
   4.120    | is_chain _  = false;
   4.121  
   4.122 -fun pretty extern_const context tabs trf tokentrf type_mode curried ast0 p0 =
   4.123 +fun pretty extern_const ctxt tabs trf tokentrf type_mode curried ast0 p0 =
   4.124    let
   4.125 -    val trans = apply_trans context "print ast translation";
   4.126 +    val trans = apply_trans ctxt "print ast translation";
   4.127  
   4.128      fun token_trans c [Ast.Variable x] =
   4.129            (case tokentrf c of
   4.130 @@ -292,7 +292,7 @@
   4.131              val (Ts, args') = synT (symbs, args);
   4.132            in
   4.133              if type_mode then (astT (t, p) @ Ts, args')
   4.134 -            else (pretty I context tabs trf tokentrf true curried t p @ Ts, args')
   4.135 +            else (pretty I ctxt tabs trf tokentrf true curried t p @ Ts, args')
   4.136            end
   4.137        | synT (String s :: symbs, args) =
   4.138            let val (Ts, args') = synT (symbs, args);
   4.139 @@ -366,15 +366,15 @@
   4.140  
   4.141  (* pretty_term_ast *)
   4.142  
   4.143 -fun pretty_term_ast extern_const context curried prtabs trf tokentrf ast =
   4.144 -  Pretty.blk (0, pretty extern_const context (mode_tabs prtabs (! print_mode))
   4.145 +fun pretty_term_ast extern_const ctxt curried prtabs trf tokentrf ast =
   4.146 +  Pretty.blk (0, pretty extern_const ctxt (mode_tabs prtabs (! print_mode))
   4.147      trf tokentrf false curried ast 0);
   4.148  
   4.149  
   4.150  (* pretty_typ_ast *)
   4.151  
   4.152 -fun pretty_typ_ast context _ prtabs trf tokentrf ast =
   4.153 -  Pretty.blk (0, pretty I context (mode_tabs prtabs (! print_mode))
   4.154 +fun pretty_typ_ast ctxt _ prtabs trf tokentrf ast =
   4.155 +  Pretty.blk (0, pretty I ctxt (mode_tabs prtabs (! print_mode))
   4.156      trf tokentrf true false ast 0);
   4.157  
   4.158  end;
     5.1 --- a/src/Pure/Syntax/syn_ext.ML	Mon Dec 11 19:05:25 2006 +0100
     5.2 +++ b/src/Pure/Syntax/syn_ext.ML	Mon Dec 11 21:39:26 2006 +0100
     5.3 @@ -42,33 +42,30 @@
     5.4        xprods: xprod list,
     5.5        consts: string list,
     5.6        prmodes: string list,
     5.7 -      parse_ast_translation:
     5.8 -        (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
     5.9 +      parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
    5.10        parse_rules: (Ast.ast * Ast.ast) list,
    5.11 -      parse_translation:
    5.12 -        (string * ((Context.generic -> term list -> term) * stamp)) list,
    5.13 +      parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
    5.14        print_translation:
    5.15 -        (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list,
    5.16 +        (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
    5.17        print_rules: (Ast.ast * Ast.ast) list,
    5.18 -      print_ast_translation:
    5.19 -        (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
    5.20 +      print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
    5.21        token_translation: (string * string * (string -> string * real)) list}
    5.22    val mfix_delims: string -> string list
    5.23    val mfix_args: string -> int
    5.24    val escape_mfix: string -> string
    5.25    val unlocalize_mfix: string -> string
    5.26    val syn_ext': bool -> (string -> bool) -> mfix list ->
    5.27 -    string list -> (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list *
    5.28 -    (string * ((Context.generic -> term list -> term) * stamp)) list *
    5.29 -    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
    5.30 -    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list
    5.31 +    string list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
    5.32 +    (string * ((Proof.context -> term list -> term) * stamp)) list *
    5.33 +    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
    5.34 +    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
    5.35      -> (string * string * (string -> string * real)) list
    5.36      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    5.37    val syn_ext: mfix list -> string list ->
    5.38 -    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list *
    5.39 -    (string * ((Context.generic -> term list -> term) * stamp)) list *
    5.40 -    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
    5.41 -    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list
    5.42 +    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
    5.43 +    (string * ((Proof.context -> term list -> term) * stamp)) list *
    5.44 +    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
    5.45 +    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list
    5.46      -> (string * string * (string -> string * real)) list
    5.47      -> (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
    5.48    val syn_ext_const_names: string list -> syn_ext
    5.49 @@ -79,10 +76,10 @@
    5.50      (string * ((bool -> typ -> term list -> term) * stamp)) list *
    5.51      (string * ((Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    5.52    val syn_ext_advanced_trfuns:
    5.53 -    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list *
    5.54 -    (string * ((Context.generic -> term list -> term) * stamp)) list *
    5.55 -    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
    5.56 -    (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    5.57 +    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
    5.58 +    (string * ((Proof.context -> term list -> term) * stamp)) list *
    5.59 +    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
    5.60 +    (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list -> syn_ext
    5.61    val syn_ext_tokentrfuns: (string * string * (string -> string * real)) list -> syn_ext
    5.62    val standard_token_markers: string list
    5.63    val pure_ext: syn_ext
    5.64 @@ -339,16 +336,13 @@
    5.65      xprods: xprod list,
    5.66      consts: string list,
    5.67      prmodes: string list,
    5.68 -    parse_ast_translation:
    5.69 -      (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
    5.70 +    parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
    5.71      parse_rules: (Ast.ast * Ast.ast) list,
    5.72 -    parse_translation:
    5.73 -      (string * ((Context.generic -> term list -> term) * stamp)) list,
    5.74 +    parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
    5.75      print_translation:
    5.76 -      (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list,
    5.77 +      (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list,
    5.78      print_rules: (Ast.ast * Ast.ast) list,
    5.79 -    print_ast_translation:
    5.80 -      (string * ((Context.generic -> Ast.ast list -> Ast.ast) * stamp)) list,
    5.81 +    print_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
    5.82      token_translation: (string * string * (string -> string * real)) list};
    5.83  
    5.84  
     6.1 --- a/src/Pure/Syntax/syntax.ML	Mon Dec 11 19:05:25 2006 +0100
     6.2 +++ b/src/Pure/Syntax/syntax.ML	Mon Dec 11 21:39:26 2006 +0100
     6.3 @@ -51,16 +51,16 @@
     6.4      (string * ((bool -> typ -> term list -> term) * stamp)) list *
     6.5      (string * ((ast list -> ast) * stamp)) list -> syntax -> syntax
     6.6    val extend_advanced_trfuns:
     6.7 -    (string * ((Context.generic -> ast list -> ast) * stamp)) list *
     6.8 -    (string * ((Context.generic -> term list -> term) * stamp)) list *
     6.9 -    (string * ((Context.generic -> bool -> typ -> term list -> term) * stamp)) list *
    6.10 -    (string * ((Context.generic -> ast list -> ast) * stamp)) list -> syntax -> syntax
    6.11 +    (string * ((Proof.context -> ast list -> ast) * stamp)) list *
    6.12 +    (string * ((Proof.context -> term list -> term) * stamp)) list *
    6.13 +    (string * ((Proof.context -> bool -> typ -> term list -> term) * stamp)) list *
    6.14 +    (string * ((Proof.context -> ast list -> ast) * stamp)) list -> syntax -> syntax
    6.15    val extend_tokentrfuns: (string * string * (string -> string * real)) list -> syntax -> syntax
    6.16    val remove_const_gram: (string -> bool) ->
    6.17      mode -> (string * typ * mixfix) list -> syntax -> syntax
    6.18 -  val extend_trrules: Context.generic -> (string -> bool) -> syntax ->
    6.19 +  val extend_trrules: Proof.context -> (string -> bool) -> syntax ->
    6.20      (string * string) trrule list -> syntax -> syntax
    6.21 -  val remove_trrules: Context.generic -> (string -> bool) -> syntax ->
    6.22 +  val remove_trrules: Proof.context -> (string -> bool) -> syntax ->
    6.23      (string * string) trrule list -> syntax -> syntax
    6.24    val extend_trrules_i: ast trrule list -> syntax -> syntax
    6.25    val remove_trrules_i: ast trrule list -> syntax -> syntax
    6.26 @@ -73,13 +73,13 @@
    6.27    val print_gram: syntax -> unit
    6.28    val print_trans: syntax -> unit
    6.29    val print_syntax: syntax -> unit
    6.30 -  val read: Context.generic -> (string -> bool) -> syntax -> typ -> string -> term list
    6.31 -  val read_typ: Context.generic -> syntax -> ((indexname * sort) list -> indexname -> sort) ->
    6.32 +  val read: Proof.context -> (string -> bool) -> syntax -> typ -> string -> term list
    6.33 +  val read_typ: Proof.context -> syntax -> ((indexname * sort) list -> indexname -> sort) ->
    6.34      (sort -> sort) -> string -> typ
    6.35 -  val read_sort: Context.generic -> syntax -> string -> sort
    6.36 -  val pretty_term: (string -> xstring) -> Context.generic -> syntax -> bool -> term -> Pretty.T
    6.37 -  val pretty_typ: Context.generic -> syntax -> typ -> Pretty.T
    6.38 -  val pretty_sort: Context.generic -> syntax -> sort -> Pretty.T
    6.39 +  val read_sort: Proof.context -> syntax -> string -> sort
    6.40 +  val pretty_term: (string -> xstring) -> Proof.context -> syntax -> bool -> term -> Pretty.T
    6.41 +  val pretty_typ: Proof.context -> syntax -> typ -> Pretty.T
    6.42 +  val pretty_sort: Proof.context -> syntax -> sort -> Pretty.T
    6.43    val ambiguity_level: int ref
    6.44    val ambiguity_is_error: bool ref
    6.45  end;
    6.46 @@ -172,12 +172,12 @@
    6.47      gram: Parser.gram,
    6.48      consts: string list,
    6.49      prmodes: string list,
    6.50 -    parse_ast_trtab: ((Context.generic -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
    6.51 +    parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
    6.52      parse_ruletab: ruletab,
    6.53 -    parse_trtab: ((Context.generic -> term list -> term) * stamp) Symtab.table,
    6.54 -    print_trtab: ((Context.generic -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
    6.55 +    parse_trtab: ((Proof.context -> term list -> term) * stamp) Symtab.table,
    6.56 +    print_trtab: ((Proof.context -> bool -> typ -> term list -> term) * stamp) list Symtab.table,
    6.57      print_ruletab: ruletab,
    6.58 -    print_ast_trtab: ((Context.generic -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
    6.59 +    print_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) list Symtab.table,
    6.60      tokentrtab: (string * (string * ((string -> string * real) * stamp)) list) list,
    6.61      prtabs: Printer.prtabs} * stamp;
    6.62  
    6.63 @@ -384,7 +384,7 @@
    6.64  val ambiguity_level = ref 1;
    6.65  val ambiguity_is_error = ref false
    6.66  
    6.67 -fun read_asts context is_logtype (Syntax (tabs, _)) xids root str =
    6.68 +fun read_asts ctxt is_logtype (Syntax (tabs, _)) xids root str =
    6.69    let
    6.70      val {lexicon, gram, parse_ast_trtab, ...} = tabs;
    6.71      val root' = if root <> "prop" andalso is_logtype root then SynExt.logic else root;
    6.72 @@ -392,41 +392,41 @@
    6.73      val pts = Parser.parse gram root' (Lexicon.tokenize lexicon xids chars);
    6.74  
    6.75      fun show_pt pt =
    6.76 -      Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts context (K NONE) [pt])));
    6.77 +      Pretty.string_of (Ast.pretty_ast (hd (SynTrans.pts_to_asts ctxt (K NONE) [pt])));
    6.78    in
    6.79      conditional (length pts > ! ambiguity_level) (fn () =>
    6.80        if ! ambiguity_is_error then error ("Ambiguous input " ^ quote str)
    6.81        else (warning ("Ambiguous input " ^ quote str ^ "\n" ^
    6.82            "produces " ^ string_of_int (length pts) ^ " parse trees.");
    6.83           List.app (warning o show_pt) pts));
    6.84 -    SynTrans.pts_to_asts context (lookup_tr parse_ast_trtab) pts
    6.85 +    SynTrans.pts_to_asts ctxt (lookup_tr parse_ast_trtab) pts
    6.86    end;
    6.87  
    6.88  
    6.89  (* read *)
    6.90  
    6.91 -fun read context is_logtype (syn as Syntax (tabs, _)) ty str =
    6.92 +fun read ctxt is_logtype (syn as Syntax (tabs, _)) ty str =
    6.93    let
    6.94      val {parse_ruletab, parse_trtab, ...} = tabs;
    6.95 -    val asts = read_asts context is_logtype syn false (SynExt.typ_to_nonterm ty) str;
    6.96 +    val asts = read_asts ctxt is_logtype syn false (SynExt.typ_to_nonterm ty) str;
    6.97    in
    6.98 -    SynTrans.asts_to_terms context (lookup_tr parse_trtab)
    6.99 +    SynTrans.asts_to_terms ctxt (lookup_tr parse_trtab)
   6.100        (map (Ast.normalize_ast (Symtab.lookup_list parse_ruletab)) asts)
   6.101    end;
   6.102  
   6.103  
   6.104  (* read types *)
   6.105  
   6.106 -fun read_typ context syn get_sort map_sort str =
   6.107 -  (case read context (K false) syn SynExt.typeT str of
   6.108 +fun read_typ ctxt syn get_sort map_sort str =
   6.109 +  (case read ctxt (K false) syn SynExt.typeT str of
   6.110      [t] => TypeExt.typ_of_term (get_sort (TypeExt.raw_term_sorts t)) map_sort t
   6.111    | _ => error "read_typ: ambiguous syntax");
   6.112  
   6.113  
   6.114  (* read sorts *)
   6.115  
   6.116 -fun read_sort context syn str =
   6.117 -  (case read context (K false) syn TypeExt.sortT str of
   6.118 +fun read_sort ctxt syn str =
   6.119 +  (case read ctxt (K false) syn TypeExt.sortT str of
   6.120      [t] => TypeExt.sort_of_term t
   6.121    | _ => error "read_sort: ambiguous syntax");
   6.122  
   6.123 @@ -462,7 +462,7 @@
   6.124    | NONE => rule);
   6.125  
   6.126  
   6.127 -fun read_pattern context is_logtype syn (root, str) =
   6.128 +fun read_pattern ctxt is_logtype syn (root, str) =
   6.129    let
   6.130      val Syntax ({consts, ...}, _) = syn;
   6.131  
   6.132 @@ -472,7 +472,7 @@
   6.133            else ast
   6.134        | constify (Ast.Appl asts) = Ast.Appl (map constify asts);
   6.135    in
   6.136 -    (case read_asts context is_logtype syn true root str of
   6.137 +    (case read_asts ctxt is_logtype syn true root str of
   6.138        [ast] => constify ast
   6.139      | _ => error ("Syntactically ambiguous input: " ^ quote str))
   6.140    end handle ERROR msg =>
   6.141 @@ -489,8 +489,8 @@
   6.142  
   6.143  val cert_rules = prep_rules I;
   6.144  
   6.145 -fun read_rules context is_logtype syn =
   6.146 -  prep_rules (read_pattern context is_logtype syn);
   6.147 +fun read_rules ctxt is_logtype syn =
   6.148 +  prep_rules (read_pattern ctxt is_logtype syn);
   6.149  
   6.150  end;
   6.151  
   6.152 @@ -498,19 +498,19 @@
   6.153  
   6.154  (** pretty terms, typs, sorts **)
   6.155  
   6.156 -fun pretty_t t_to_ast prt_t context (syn as Syntax (tabs, _)) curried t =
   6.157 +fun pretty_t t_to_ast prt_t ctxt (syn as Syntax (tabs, _)) curried t =
   6.158    let
   6.159      val {print_trtab, print_ruletab, print_ast_trtab, tokentrtab, prtabs, ...} = tabs;
   6.160 -    val ast = t_to_ast context (lookup_tr' print_trtab) t;
   6.161 +    val ast = t_to_ast ctxt (lookup_tr' print_trtab) t;
   6.162    in
   6.163 -    prt_t context curried prtabs (lookup_tr' print_ast_trtab)
   6.164 +    prt_t ctxt curried prtabs (lookup_tr' print_ast_trtab)
   6.165        (lookup_tokentr tokentrtab (! print_mode))
   6.166        (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast)
   6.167    end;
   6.168  
   6.169  val pretty_term = pretty_t Printer.term_to_ast o Printer.pretty_term_ast;
   6.170 -fun pretty_typ context syn = pretty_t Printer.typ_to_ast Printer.pretty_typ_ast context syn false;
   6.171 -fun pretty_sort context syn = pretty_t Printer.sort_to_ast Printer.pretty_typ_ast context syn false;
   6.172 +fun pretty_typ ctxt syn = pretty_t Printer.typ_to_ast Printer.pretty_typ_ast ctxt syn false;
   6.173 +fun pretty_sort ctxt syn = pretty_t Printer.sort_to_ast Printer.pretty_typ_ast ctxt syn false;
   6.174  
   6.175  
   6.176  
   6.177 @@ -529,11 +529,11 @@
   6.178  fun remove_const_gram is_logtype prmode decls =
   6.179    remove_syntax prmode (Mixfix.syn_ext_consts is_logtype decls);
   6.180  
   6.181 -fun extend_trrules context is_logtype syn =
   6.182 -  ext_syntax SynExt.syn_ext_rules o read_rules context is_logtype syn;
   6.183 +fun extend_trrules ctxt is_logtype syn =
   6.184 +  ext_syntax SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
   6.185  
   6.186 -fun remove_trrules context is_logtype syn =
   6.187 -  remove_syntax default_mode o SynExt.syn_ext_rules o read_rules context is_logtype syn;
   6.188 +fun remove_trrules ctxt is_logtype syn =
   6.189 +  remove_syntax default_mode o SynExt.syn_ext_rules o read_rules ctxt is_logtype syn;
   6.190  
   6.191  val extend_trrules_i = ext_syntax SynExt.syn_ext_rules o cert_rules;
   6.192  val remove_trrules_i = remove_syntax default_mode o SynExt.syn_ext_rules o cert_rules;
     7.1 --- a/src/Pure/sign.ML	Mon Dec 11 19:05:25 2006 +0100
     7.2 +++ b/src/Pure/sign.ML	Mon Dec 11 21:39:26 2006 +0100
     7.3 @@ -36,12 +36,12 @@
     7.4    val add_trfunsT:
     7.5      (string * (bool -> typ -> term list -> term)) list -> theory -> theory
     7.6    val add_advanced_trfuns:
     7.7 -    (string * (Context.generic -> ast list -> ast)) list *
     7.8 -    (string * (Context.generic -> term list -> term)) list *
     7.9 -    (string * (Context.generic -> term list -> term)) list *
    7.10 -    (string * (Context.generic -> ast list -> ast)) list -> theory -> theory
    7.11 +    (string * (Proof.context -> ast list -> ast)) list *
    7.12 +    (string * (Proof.context -> term list -> term)) list *
    7.13 +    (string * (Proof.context -> term list -> term)) list *
    7.14 +    (string * (Proof.context -> ast list -> ast)) list -> theory -> theory
    7.15    val add_advanced_trfunsT:
    7.16 -    (string * (Context.generic -> bool -> typ -> term list -> term)) list -> theory -> theory
    7.17 +    (string * (Proof.context -> bool -> typ -> term list -> term)) list -> theory -> theory
    7.18    val add_tokentrfuns:
    7.19      (string * string * (string -> string * real)) list -> theory -> theory
    7.20    val add_mode_tokentrfuns: string -> (string * (string -> string * real)) list
    7.21 @@ -133,7 +133,7 @@
    7.22    val intern_term: theory -> term -> term
    7.23    val extern_term: (string -> xstring) -> theory -> term -> term
    7.24    val intern_tycons: theory -> typ -> typ
    7.25 -  val pretty_term': Context.generic -> Syntax.syntax -> (string -> xstring) -> term -> Pretty.T
    7.26 +  val pretty_term': Proof.context -> Syntax.syntax -> (string -> xstring) -> term -> Pretty.T
    7.27    val pretty_term: theory -> term -> Pretty.T
    7.28    val pretty_typ: theory -> typ -> Pretty.T
    7.29    val pretty_sort: theory -> sort -> Pretty.T
    7.30 @@ -161,15 +161,14 @@
    7.31    val no_vars: Pretty.pp -> term -> term
    7.32    val cert_def: Pretty.pp -> term -> (string * typ) * term
    7.33    val read_class: theory -> xstring -> class
    7.34 -  val read_sort': Syntax.syntax -> Context.generic -> string -> sort
    7.35 +  val read_sort': Syntax.syntax -> Proof.context -> string -> sort
    7.36    val read_sort: theory -> string -> sort
    7.37    val read_arity: theory -> xstring * string list * string -> arity
    7.38    val cert_arity: theory -> arity -> arity
    7.39 -  val read_typ': Syntax.syntax -> Context.generic ->
    7.40 +  val read_typ': Syntax.syntax -> Proof.context -> (indexname -> sort option) -> string -> typ
    7.41 +  val read_typ_syntax': Syntax.syntax -> Proof.context ->
    7.42      (indexname -> sort option) -> string -> typ
    7.43 -  val read_typ_syntax': Syntax.syntax -> Context.generic ->
    7.44 -    (indexname -> sort option) -> string -> typ
    7.45 -  val read_typ_abbrev': Syntax.syntax -> Context.generic ->
    7.46 +  val read_typ_abbrev': Syntax.syntax -> Proof.context ->
    7.47      (indexname -> sort option) -> string -> typ
    7.48    val read_typ: theory * (indexname -> sort option) -> string -> typ
    7.49    val read_typ_syntax: theory * (indexname -> sort option) -> string -> typ
    7.50 @@ -183,7 +182,7 @@
    7.51      (indexname -> sort option) -> Name.context -> bool
    7.52      -> term list * typ -> term * (indexname * typ) list
    7.53    val read_def_terms': Pretty.pp -> (string -> bool) -> Syntax.syntax -> Consts.T ->
    7.54 -    Context.generic -> (indexname -> typ option) * (indexname -> sort option) ->
    7.55 +    Proof.context -> (indexname -> typ option) * (indexname -> sort option) ->
    7.56      Name.context -> bool -> (string * typ) list -> term list * (indexname * typ) list
    7.57    val read_def_terms:
    7.58      theory * (indexname -> typ option) * (indexname -> sort option) ->
    7.59 @@ -371,16 +370,19 @@
    7.60  
    7.61  (** pretty printing of terms, types etc. **)
    7.62  
    7.63 -fun pretty_term' context syn ext t =
    7.64 -  let val curried = Context.exists_name Context.CPureN (Context.theory_of context)
    7.65 -  in Syntax.pretty_term ext context syn curried t end;
    7.66 +fun pretty_term' ctxt syn ext t =
    7.67 +  let val curried = Context.exists_name Context.CPureN (ProofContext.theory_of ctxt)
    7.68 +  in Syntax.pretty_term ext ctxt syn curried t end;
    7.69  
    7.70  fun pretty_term thy t =
    7.71 -  pretty_term' (Context.Theory thy) (syn_of thy) (Consts.extern (consts_of thy))
    7.72 +  pretty_term' (ProofContext.init thy) (syn_of thy) (Consts.extern (consts_of thy))
    7.73      (extern_term (Consts.extern_early (consts_of thy)) thy t);
    7.74  
    7.75 -fun pretty_typ thy T = Syntax.pretty_typ (Context.Theory thy) (syn_of thy) (extern_typ thy T);
    7.76 -fun pretty_sort thy S = Syntax.pretty_sort (Context.Theory thy) (syn_of thy) (extern_sort thy S);
    7.77 +fun pretty_typ thy T =
    7.78 +  Syntax.pretty_typ (ProofContext.init thy) (syn_of thy) (extern_typ thy T);
    7.79 +
    7.80 +fun pretty_sort thy S =
    7.81 +  Syntax.pretty_sort (ProofContext.init thy) (syn_of thy) (extern_sort thy S);
    7.82  
    7.83  fun pretty_classrel thy cs = Pretty.block (flat
    7.84    (separate [Pretty.str " <", Pretty.brk 1] (map (single o pretty_sort thy o single) cs)));
    7.85 @@ -510,14 +512,14 @@
    7.86  fun read_class thy c = certify_class thy (intern_class thy c)
    7.87    handle TYPE (msg, _, _) => error msg;
    7.88  
    7.89 -fun read_sort' syn context str =
    7.90 +fun read_sort' syn ctxt str =
    7.91    let
    7.92 -    val thy = Context.theory_of context;
    7.93 +    val thy = ProofContext.theory_of ctxt;
    7.94      val _ = Context.check_thy thy;
    7.95 -    val S = intern_sort thy (Syntax.read_sort context syn str);
    7.96 +    val S = intern_sort thy (Syntax.read_sort ctxt syn str);
    7.97    in certify_sort thy S handle TYPE (msg, _, _) => error msg end;
    7.98  
    7.99 -fun read_sort thy str = read_sort' (syn_of thy) (Context.Theory thy) str;
   7.100 +fun read_sort thy str = read_sort' (syn_of thy) (ProofContext.init thy) str;
   7.101  
   7.102  
   7.103  (* type arities *)
   7.104 @@ -534,17 +536,17 @@
   7.105  
   7.106  local
   7.107  
   7.108 -fun gen_read_typ' cert syn context def_sort str =
   7.109 +fun gen_read_typ' cert syn ctxt def_sort str =
   7.110    let
   7.111 -    val thy = Context.theory_of context;
   7.112 +    val thy = ProofContext.theory_of ctxt;
   7.113      val _ = Context.check_thy thy;
   7.114      val get_sort = TypeInfer.get_sort (tsig_of thy) def_sort (intern_sort thy);
   7.115 -    val T = intern_tycons thy (Syntax.read_typ context syn get_sort (intern_sort thy) str);
   7.116 +    val T = intern_tycons thy (Syntax.read_typ ctxt syn get_sort (intern_sort thy) str);
   7.117    in cert thy T handle TYPE (msg, _, _) => error msg end
   7.118    handle ERROR msg => cat_error msg ("The error(s) above occurred in type " ^ quote str);
   7.119  
   7.120  fun gen_read_typ cert (thy, def_sort) str =
   7.121 -  gen_read_typ' cert (syn_of thy) (Context.Theory thy) def_sort str;
   7.122 +  gen_read_typ' cert (syn_of thy) (ProofContext.init thy) def_sort str;
   7.123  
   7.124  in
   7.125  
   7.126 @@ -620,12 +622,12 @@
   7.127  
   7.128  (* read_def_terms -- read terms and infer types *)    (*exception ERROR*)
   7.129  
   7.130 -fun read_def_terms' pp is_logtype syn consts context (types, sorts) used freeze sTs =
   7.131 +fun read_def_terms' pp is_logtype syn consts ctxt (types, sorts) used freeze sTs =
   7.132    let
   7.133 -    val thy = Context.theory_of context;
   7.134 +    val thy = ProofContext.theory_of ctxt;
   7.135      fun read (s, T) =
   7.136        let val T' = certify_typ thy T handle TYPE (msg, _, _) => error msg
   7.137 -      in (Syntax.read context is_logtype syn T' s, T') end;
   7.138 +      in (Syntax.read ctxt is_logtype syn T' s, T') end;
   7.139    in infer_types_simult pp thy consts types sorts used freeze (map read sTs) end;
   7.140  
   7.141  fun read_def_terms (thy, types, sorts) used freeze sTs =
   7.142 @@ -635,7 +637,7 @@
   7.143      val cert_consts = Consts.certify pp (tsig_of thy) consts;
   7.144      val (ts, inst) =
   7.145        read_def_terms' pp (is_logtype thy) (syn_of thy) consts
   7.146 -        (Context.Theory thy) (types, sorts) (Name.make_context used) freeze sTs;
   7.147 +        (ProofContext.init thy) (types, sorts) (Name.make_context used) freeze sTs;
   7.148    in (map cert_consts ts, inst) end;
   7.149  
   7.150  fun simple_read_term thy T s =
   7.151 @@ -827,7 +829,7 @@
   7.152  local
   7.153  
   7.154  fun advancedT false = ""
   7.155 -  | advancedT true = "Context.generic -> ";
   7.156 +  | advancedT true = "Proof.context -> ";
   7.157  
   7.158  fun advancedN false = ""
   7.159    | advancedN true = "advanced_";
   7.160 @@ -870,7 +872,7 @@
   7.161  
   7.162  fun gen_trrules f args thy = thy |> map_syn (fn syn =>
   7.163    let val rules = map (Syntax.map_trrule (apfst (intern_type thy))) args
   7.164 -  in f (Context.Theory thy) (is_logtype thy) syn rules syn end);
   7.165 +  in f (ProofContext.init thy) (is_logtype thy) syn rules syn end);
   7.166  
   7.167  val add_trrules = gen_trrules Syntax.extend_trrules;
   7.168  val del_trrules = gen_trrules Syntax.remove_trrules;
     8.1 --- a/src/Pure/theory.ML	Mon Dec 11 19:05:25 2006 +0100
     8.2 +++ b/src/Pure/theory.ML	Mon Dec 11 21:39:26 2006 +0100
     8.3 @@ -178,7 +178,7 @@
     8.4  
     8.5  fun read_def_axm (thy, types, sorts) used (name, str) =
     8.6    let
     8.7 -    val ts = Syntax.read (Context.Theory thy) (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
     8.8 +    val ts = Syntax.read (ProofContext.init thy) (Sign.is_logtype thy) (Sign.syn_of thy) propT str;
     8.9      val (t, _) =
    8.10        Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy)
    8.11          types sorts (Name.make_context used) true (ts, propT);