tuned;
authorwenzelm
Fri Dec 19 12:36:50 2014 +0100 (2014-12-19)
changeset 5915071b416020f42
parent 59149 0070053570c4
child 59151 a012574b78e7
tuned;
src/Pure/Isar/class.ML
src/Pure/Isar/overloading.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/toplevel.ML
src/Pure/assumption.ML
src/Pure/variable.ML
src/Tools/Code/code_runtime.ML
     1.1 --- a/src/Pure/Isar/class.ML	Thu Dec 18 21:10:39 2014 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Fri Dec 19 12:36:50 2014 +0100
     1.3 @@ -484,21 +484,23 @@
     1.4      (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*)
     1.5  }
     1.6  
     1.7 +fun make_instantiation (arities, params) =
     1.8 +  Instantiation {arities = arities, params = params};
     1.9 +
    1.10 +val empty_instantiation = make_instantiation (([], [], []), []);
    1.11 +
    1.12  structure Instantiation = Proof_Data
    1.13  (
    1.14    type T = instantiation;
    1.15 -  fun init _ = Instantiation {arities = ([], [], []), params = []};
    1.16 +  fun init _ = empty_instantiation;
    1.17  );
    1.18  
    1.19 -fun mk_instantiation (arities, params) =
    1.20 -  Instantiation {arities = arities, params = params};
    1.21 -
    1.22  val get_instantiation =
    1.23    (fn Instantiation data => data) o Instantiation.get o Local_Theory.target_of;
    1.24  
    1.25  fun map_instantiation f =
    1.26    (Local_Theory.target o Instantiation.map)
    1.27 -    (fn Instantiation {arities, params} => mk_instantiation (f (arities, params)));
    1.28 +    (fn Instantiation {arities, params} => make_instantiation (f (arities, params)));
    1.29  
    1.30  fun the_instantiation lthy =
    1.31    (case get_instantiation lthy of
    1.32 @@ -624,7 +626,7 @@
    1.33      thy
    1.34      |> Sign.change_begin
    1.35      |> Proof_Context.init_global
    1.36 -    |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
    1.37 +    |> Instantiation.put (make_instantiation ((tycos, vs, sort), params))
    1.38      |> fold (Variable.declare_typ o TFree) vs
    1.39      |> fold (Variable.declare_names o Free o snd) params
    1.40      |> (Overloading.map_improvable_syntax o apfst)
     2.1 --- a/src/Pure/Isar/overloading.ML	Thu Dec 18 21:10:39 2014 +0100
     2.2 +++ b/src/Pure/Isar/overloading.ML	Fri Dec 19 12:36:50 2014 +0100
     2.3 @@ -36,7 +36,7 @@
     2.4      unchecks: (term * term) list,
     2.5      passed: bool
     2.6    };
     2.7 -  fun init _ = {
     2.8 +  val empty: T = {
     2.9      primary_constraints = [],
    2.10      secondary_constraints = [],
    2.11      improve = K NONE,
    2.12 @@ -45,6 +45,7 @@
    2.13      unchecks = [],
    2.14      passed = true
    2.15    };
    2.16 +  fun init _ = empty;
    2.17  );
    2.18  
    2.19  fun map_improvable_syntax f = Improvable_Syntax.map (fn {primary_constraints,
     3.1 --- a/src/Pure/Isar/proof.ML	Thu Dec 18 21:10:39 2014 +0100
     3.2 +++ b/src/Pure/Isar/proof.ML	Fri Dec 19 12:36:50 2014 +0100
     3.3 @@ -1100,8 +1100,7 @@
     3.4  structure Result = Proof_Data
     3.5  (
     3.6    type T = thm option;
     3.7 -  val empty = NONE;
     3.8 -  fun init _ = empty;
     3.9 +  fun init _ = NONE;
    3.10  );
    3.11  
    3.12  fun the_result ctxt =
     4.1 --- a/src/Pure/Isar/toplevel.ML	Thu Dec 18 21:10:39 2014 +0100
     4.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Dec 19 12:36:50 2014 +0100
     4.3 @@ -633,8 +633,7 @@
     4.4  structure Result = Proof_Data
     4.5  (
     4.6    type T = result;
     4.7 -  val empty: T = Result_List [];
     4.8 -  fun init _ = empty;
     4.9 +  fun init _ = Result_List [];
    4.10  );
    4.11  
    4.12  val get_result = Result.get o Proof.context_of;
     5.1 --- a/src/Pure/assumption.ML	Thu Dec 18 21:10:39 2014 +0100
     5.2 +++ b/src/Pure/assumption.ML	Fri Dec 19 12:36:50 2014 +0100
     5.3 @@ -64,11 +64,12 @@
     5.4    prems: thm list};                     (*prems: A |- norm_hhf A*)
     5.5  
     5.6  fun make_data (assms, prems) = Data {assms = assms, prems = prems};
     5.7 +val empty_data = make_data ([], []);
     5.8  
     5.9  structure Data = Proof_Data
    5.10  (
    5.11    type T = data;
    5.12 -  fun init _ = make_data ([], []);
    5.13 +  fun init _ = empty_data;
    5.14  );
    5.15  
    5.16  fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems)));
     6.1 --- a/src/Pure/variable.ML	Thu Dec 18 21:10:39 2014 +0100
     6.2 +++ b/src/Pure/variable.ML	Fri Dec 19 12:36:50 2014 +0100
     6.3 @@ -104,12 +104,14 @@
     6.4    Data {is_body = is_body, names = names, consts = consts, bounds = bounds, fixes = fixes,
     6.5      binds = binds, type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints};
     6.6  
     6.7 +val empty_data =
     6.8 +  make_data (false, Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty,
     6.9 +    Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty));
    6.10 +
    6.11  structure Data = Proof_Data
    6.12  (
    6.13    type T = data;
    6.14 -  fun init _ =
    6.15 -    make_data (false, Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty,
    6.16 -      Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty));
    6.17 +  fun init _ = empty_data;
    6.18  );
    6.19  
    6.20  fun map_data f =
     7.1 --- a/src/Tools/Code/code_runtime.ML	Thu Dec 18 21:10:39 2014 +0100
     7.2 +++ b/src/Tools/Code/code_runtime.ML	Fri Dec 19 12:36:50 2014 +0100
     7.3 @@ -336,7 +336,8 @@
     7.4  (
     7.5    type T = (string list * string list) * (bool
     7.6      * (string * (string * string) list) lazy);
     7.7 -  fun init _ = (([], []), (true, (Lazy.value ("", []))));
     7.8 +  val empty: T = (([], []), (true, (Lazy.value ("", []))));
     7.9 +  fun init _ = empty;
    7.10  );
    7.11  
    7.12  val is_first_occ = fst o snd o Code_Antiq_Data.get;