dropped local tsigs
authorhaftmann
Fri Mar 07 13:53:09 2008 +0100 (2008-03-07 ago)
changeset 26240cc630a75b62a
parent 26239 e105d24d15c1
child 26241 b7d8c2338585
dropped local tsigs
src/Pure/Isar/proof_context.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Mar 07 13:53:08 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Mar 07 13:53:09 2008 +0100
     1.3 @@ -10,7 +10,6 @@
     1.4  signature PROOF_CONTEXT =
     1.5  sig
     1.6    val theory_of: Proof.context -> theory
     1.7 -  val tsig_of: Proof.context -> Type.tsig
     1.8    val init: theory -> Proof.context
     1.9    type mode
    1.10    val mode_default: mode
    1.11 @@ -27,7 +26,6 @@
    1.12    val consts_of: Proof.context -> Consts.T
    1.13    val const_syntax_name: Proof.context -> string -> string
    1.14    val the_const_constraint: Proof.context -> string -> typ
    1.15 -  val add_arity: arity -> Proof.context -> Proof.context
    1.16    val set_syntax_mode: Syntax.mode -> Proof.context -> Proof.context
    1.17    val restore_syntax_mode: Proof.context -> Proof.context -> Proof.context
    1.18    val theorems_of: Proof.context -> thm list NameSpace.table
    1.19 @@ -185,15 +183,14 @@
    1.20  datatype ctxt =
    1.21    Ctxt of
    1.22     {mode: mode,                                       (*inner syntax mode*)
    1.23 -    tsig: Type.tsig,                                  (*local type signature*)
    1.24      naming: NameSpace.naming,                         (*local naming conventions*)
    1.25      syntax: LocalSyntax.T,                            (*local syntax*)
    1.26      consts: Consts.T * Consts.T,                      (*local/global consts*)
    1.27      thms: thm list NameSpace.table * FactIndex.T,     (*local thms*)
    1.28      cases: (string * (RuleCases.T * bool)) list};     (*local contexts*)
    1.29  
    1.30 -fun make_ctxt (mode, tsig, naming, syntax, consts, thms, cases) =
    1.31 -  Ctxt {mode = mode, tsig = tsig, naming = naming, syntax = syntax,
    1.32 +fun make_ctxt (mode, naming, syntax, consts, thms, cases) =
    1.33 +  Ctxt {mode = mode, naming = naming, syntax = syntax,
    1.34      consts = consts, thms = thms, cases = cases};
    1.35  
    1.36  val local_naming = NameSpace.default_naming |> NameSpace.add_path "local";
    1.37 @@ -202,7 +199,7 @@
    1.38  (
    1.39    type T = ctxt;
    1.40    fun init thy =
    1.41 -    make_ctxt (mode_default, Sign.tsig_of thy, local_naming, LocalSyntax.init thy,
    1.42 +    make_ctxt (mode_default, local_naming, LocalSyntax.init thy,
    1.43        (Sign.consts_of thy, Sign.consts_of thy),
    1.44        (NameSpace.empty_table, FactIndex.empty), []);
    1.45  );
    1.46 @@ -210,39 +207,35 @@
    1.47  fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
    1.48  
    1.49  fun map_context f =
    1.50 -  ContextData.map (fn Ctxt {mode, tsig, naming, syntax, consts, thms, cases} =>
    1.51 -    make_ctxt (f (mode, tsig, naming, syntax, consts, thms, cases)));
    1.52 +  ContextData.map (fn Ctxt {mode, naming, syntax, consts, thms, cases} =>
    1.53 +    make_ctxt (f (mode, naming, syntax, consts, thms, cases)));
    1.54  
    1.55 -fun set_mode mode = map_context (fn (_, tsig, naming, syntax, consts, thms, cases) =>
    1.56 -  (mode, tsig, naming, syntax, consts, thms, cases));
    1.57 +fun set_mode mode = map_context (fn (_, naming, syntax, consts, thms, cases) =>
    1.58 +  (mode, naming, syntax, consts, thms, cases));
    1.59  
    1.60  fun map_mode f =
    1.61 -  map_context (fn (Mode {stmt, pattern, schematic, abbrev}, tsig, naming, syntax, consts, thms, cases) =>
    1.62 -    (make_mode (f (stmt, pattern, schematic, abbrev)), tsig, naming, syntax, consts, thms, cases));
    1.63 -
    1.64 -fun map_tsig f =
    1.65 -  map_context (fn (mode, tsig, naming, syntax, consts, thms, cases) =>
    1.66 -    (mode, f tsig, naming, syntax, consts, thms, cases));
    1.67 +  map_context (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, consts, thms, cases) =>
    1.68 +    (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, consts, thms, cases));
    1.69  
    1.70  fun map_naming f =
    1.71 -  map_context (fn (mode, tsig, naming, syntax, consts, thms, cases) =>
    1.72 -    (mode, tsig, f naming, syntax, consts, thms, cases));
    1.73 +  map_context (fn (mode, naming, syntax, consts, thms, cases) =>
    1.74 +    (mode, f naming, syntax, consts, thms, cases));
    1.75  
    1.76  fun map_syntax f =
    1.77 -  map_context (fn (mode, tsig, naming, syntax, consts, thms, cases) =>
    1.78 -    (mode, tsig, naming, f syntax, consts, thms, cases));
    1.79 +  map_context (fn (mode, naming, syntax, consts, thms, cases) =>
    1.80 +    (mode, naming, f syntax, consts, thms, cases));
    1.81  
    1.82  fun map_consts f =
    1.83 -  map_context (fn (mode, tsig, naming, syntax, consts, thms, cases) =>
    1.84 -    (mode, tsig, naming, syntax, f consts, thms, cases));
    1.85 +  map_context (fn (mode, naming, syntax, consts, thms, cases) =>
    1.86 +    (mode, naming, syntax, f consts, thms, cases));
    1.87  
    1.88  fun map_thms f =
    1.89 -  map_context (fn (mode, tsig, naming, syntax, consts, thms, cases) =>
    1.90 -    (mode, tsig, naming, syntax, consts, f thms, cases));
    1.91 +  map_context (fn (mode, naming, syntax, consts, thms, cases) =>
    1.92 +    (mode, naming, syntax, consts, f thms, cases));
    1.93  
    1.94  fun map_cases f =
    1.95 -  map_context (fn (mode, tsig, naming, syntax, consts, thms, cases) =>
    1.96 -    (mode, tsig, naming, syntax, consts, thms, f cases));
    1.97 +  map_context (fn (mode, naming, syntax, consts, thms, cases) =>
    1.98 +    (mode, naming, syntax, consts, thms, f cases));
    1.99  
   1.100  val get_mode = #mode o rep_context;
   1.101  fun restore_mode ctxt = set_mode (get_mode ctxt);
   1.102 @@ -253,7 +246,6 @@
   1.103  val naming_of = #naming o rep_context;
   1.104  val full_name = NameSpace.full o naming_of;
   1.105  
   1.106 -val tsig_of = #tsig o rep_context;
   1.107  val syntax_of = #syntax o rep_context;
   1.108  val syn_of = LocalSyntax.syn_of o syntax_of;
   1.109  val set_syntax_mode = map_syntax o LocalSyntax.set_mode;
   1.110 @@ -401,10 +393,6 @@
   1.111    fold_map inferred_param (rev (map #2 (Variable.fixes_of ctxt))) ctxt;
   1.112  
   1.113  
   1.114 -(* type signature *)
   1.115 -
   1.116 -fun add_arity arity ctxt = ctxt |> map_tsig (Type.add_arity (Syntax.pp ctxt) arity);
   1.117 -
   1.118  (* type and constant names *)
   1.119  
   1.120  fun read_tyname ctxt c =
   1.121 @@ -438,6 +426,8 @@
   1.122  
   1.123  (* local abbreviations *)
   1.124  
   1.125 +val tsig_of = Sign.tsig_of o ProofContext.theory_of;
   1.126 +
   1.127  local
   1.128  
   1.129  fun certify_consts ctxt =