tuned;
authorwenzelm
Sun Nov 27 21:53:38 2011 +0100 (2011-11-27)
changeset 45650d314a4e8038f
parent 45649 2d995773da1a
child 45651 172aa230ce69
tuned;
src/Pure/Isar/proof_context.ML
src/Pure/assumption.ML
src/Pure/variable.ML
     1.1 --- a/src/Pure/Isar/proof_context.ML	Sun Nov 27 14:40:08 2011 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Nov 27 21:53:38 2011 +0100
     1.3 @@ -188,8 +188,8 @@
     1.4  
     1.5  (** Isar proof context information **)
     1.6  
     1.7 -datatype ctxt =
     1.8 -  Ctxt of
     1.9 +datatype data =
    1.10 +  Data of
    1.11     {mode: mode,                  (*inner syntax mode*)
    1.12      naming: Name_Space.naming,   (*local naming conventions*)
    1.13      syntax: Local_Syntax.T,      (*local syntax*)
    1.14 @@ -198,83 +198,83 @@
    1.15      facts: Facts.T,              (*local facts*)
    1.16      cases: (string * (Rule_Cases.T * bool)) list};    (*named case contexts*)
    1.17  
    1.18 -fun make_ctxt (mode, naming, syntax, tsig, consts, facts, cases) =
    1.19 -  Ctxt {mode = mode, naming = naming, syntax = syntax,
    1.20 +fun make_data (mode, naming, syntax, tsig, consts, facts, cases) =
    1.21 +  Data {mode = mode, naming = naming, syntax = syntax,
    1.22      tsig = tsig, consts = consts, facts = facts, cases = cases};
    1.23  
    1.24  val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
    1.25  
    1.26  structure Data = Proof_Data
    1.27  (
    1.28 -  type T = ctxt;
    1.29 +  type T = data;
    1.30    fun init thy =
    1.31 -    make_ctxt (mode_default, local_naming, Local_Syntax.init thy,
    1.32 +    make_data (mode_default, local_naming, Local_Syntax.init thy,
    1.33        (Sign.tsig_of thy, Sign.tsig_of thy),
    1.34        (Sign.consts_of thy, Sign.consts_of thy), Facts.empty, []);
    1.35  );
    1.36  
    1.37 -fun rep_context ctxt = Data.get ctxt |> (fn Ctxt args => args);
    1.38 +fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
    1.39  
    1.40 -fun map_context f =
    1.41 -  Data.map (fn Ctxt {mode, naming, syntax, tsig, consts, facts, cases} =>
    1.42 -    make_ctxt (f (mode, naming, syntax, tsig, consts, facts, cases)));
    1.43 +fun map_data f =
    1.44 +  Data.map (fn Data {mode, naming, syntax, tsig, consts, facts, cases} =>
    1.45 +    make_data (f (mode, naming, syntax, tsig, consts, facts, cases)));
    1.46  
    1.47 -fun set_mode mode = map_context (fn (_, naming, syntax, tsig, consts, facts, cases) =>
    1.48 +fun set_mode mode = map_data (fn (_, naming, syntax, tsig, consts, facts, cases) =>
    1.49    (mode, naming, syntax, tsig, consts, facts, cases));
    1.50  
    1.51  fun map_mode f =
    1.52 -  map_context (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, tsig, consts, facts, cases) =>
    1.53 +  map_data (fn (Mode {stmt, pattern, schematic, abbrev}, naming, syntax, tsig, consts, facts, cases) =>
    1.54      (make_mode (f (stmt, pattern, schematic, abbrev)), naming, syntax, tsig, consts, facts, cases));
    1.55  
    1.56  fun map_naming f =
    1.57 -  map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.58 +  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.59      (mode, f naming, syntax, tsig, consts, facts, cases));
    1.60  
    1.61  fun map_syntax f =
    1.62 -  map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.63 +  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.64      (mode, naming, f syntax, tsig, consts, facts, cases));
    1.65  
    1.66  fun map_tsig f =
    1.67 -  map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.68 +  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.69      (mode, naming, syntax, f tsig, consts, facts, cases));
    1.70  
    1.71  fun map_consts f =
    1.72 -  map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.73 +  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.74      (mode, naming, syntax, tsig, f consts, facts, cases));
    1.75  
    1.76  fun map_facts f =
    1.77 -  map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.78 +  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.79      (mode, naming, syntax, tsig, consts, f facts, cases));
    1.80  
    1.81  fun map_cases f =
    1.82 -  map_context (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.83 +  map_data (fn (mode, naming, syntax, tsig, consts, facts, cases) =>
    1.84      (mode, naming, syntax, tsig, consts, facts, f cases));
    1.85  
    1.86 -val get_mode = #mode o rep_context;
    1.87 +val get_mode = #mode o rep_data;
    1.88  val restore_mode = set_mode o get_mode;
    1.89  val abbrev_mode = get_mode #> (fn Mode {abbrev, ...} => abbrev);
    1.90  
    1.91  fun set_stmt stmt =
    1.92    map_mode (fn (_, pattern, schematic, abbrev) => (stmt, pattern, schematic, abbrev));
    1.93  
    1.94 -val naming_of = #naming o rep_context;
    1.95 +val naming_of = #naming o rep_data;
    1.96  val restore_naming = map_naming o K o naming_of
    1.97  val full_name = Name_Space.full_name o naming_of;
    1.98  
    1.99 -val syntax_of = #syntax o rep_context;
   1.100 +val syntax_of = #syntax o rep_data;
   1.101  val syn_of = Local_Syntax.syn_of o syntax_of;
   1.102  val set_syntax_mode = map_syntax o Local_Syntax.set_mode;
   1.103  val restore_syntax_mode = map_syntax o Local_Syntax.restore_mode o syntax_of;
   1.104  
   1.105 -val tsig_of = #1 o #tsig o rep_context;
   1.106 +val tsig_of = #1 o #tsig o rep_data;
   1.107  val set_defsort = map_tsig o apfst o Type.set_defsort;
   1.108  fun default_sort ctxt = the_default (Type.defaultS (tsig_of ctxt)) o Variable.def_sort ctxt;
   1.109  
   1.110 -val consts_of = #1 o #consts o rep_context;
   1.111 +val consts_of = #1 o #consts o rep_data;
   1.112  val the_const_constraint = Consts.the_constraint o consts_of;
   1.113  
   1.114 -val facts_of = #facts o rep_context;
   1.115 -val cases_of = #cases o rep_context;
   1.116 +val facts_of = #facts o rep_data;
   1.117 +val cases_of = #cases o rep_data;
   1.118  
   1.119  
   1.120  (* name spaces *)
   1.121 @@ -1134,7 +1134,7 @@
   1.122  fun pretty_abbrevs show_globals ctxt =
   1.123    let
   1.124      val ((space, consts), (_, globals)) =
   1.125 -      pairself (#constants o Consts.dest) (#consts (rep_context ctxt));
   1.126 +      pairself (#constants o Consts.dest) (#consts (rep_data ctxt));
   1.127      fun add_abbr (_, (_, NONE)) = I
   1.128        | add_abbr (c, (T, SOME t)) =
   1.129            if not show_globals andalso Symtab.defined globals c then I
     2.1 --- a/src/Pure/assumption.ML	Sun Nov 27 14:40:08 2011 +0100
     2.2 +++ b/src/Pure/assumption.ML	Sun Nov 27 21:53:38 2011 +0100
     2.3 @@ -67,7 +67,7 @@
     2.4  );
     2.5  
     2.6  fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
     2.7 -fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
     2.8 +fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
     2.9  
    2.10  
    2.11  (* all assumptions *)
     3.1 --- a/src/Pure/variable.ML	Sun Nov 27 14:40:08 2011 +0100
     3.2 +++ b/src/Pure/variable.ML	Sun Nov 27 21:53:38 2011 +0100
     3.3 @@ -144,7 +144,7 @@
     3.4    map_data (fn (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, constraints) =>
     3.5      (is_body, names, consts, fixes, binds, type_occs, maxidx, sorts, f constraints));
     3.6  
     3.7 -fun rep_data ctxt = Data.get ctxt |> (fn Data args => args);
     3.8 +fun rep_data ctxt = Data.get ctxt |> (fn Data rep => rep);
     3.9  
    3.10  val is_body = #is_body o rep_data;
    3.11