# HG changeset patch # User wenzelm # Date 1418989010 -3600 # Node ID 71b416020f423fbc480c215d32011364fb71cce4 # Parent 0070053570c41383378652ec0d56625b31b63a26 tuned; diff -r 0070053570c4 -r 71b416020f42 src/Pure/Isar/class.ML --- a/src/Pure/Isar/class.ML Thu Dec 18 21:10:39 2014 +0100 +++ b/src/Pure/Isar/class.ML Fri Dec 19 12:36:50 2014 +0100 @@ -484,21 +484,23 @@ (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*) } +fun make_instantiation (arities, params) = + Instantiation {arities = arities, params = params}; + +val empty_instantiation = make_instantiation (([], [], []), []); + structure Instantiation = Proof_Data ( type T = instantiation; - fun init _ = Instantiation {arities = ([], [], []), params = []}; + fun init _ = empty_instantiation; ); -fun mk_instantiation (arities, params) = - Instantiation {arities = arities, params = params}; - val get_instantiation = (fn Instantiation data => data) o Instantiation.get o Local_Theory.target_of; fun map_instantiation f = (Local_Theory.target o Instantiation.map) - (fn Instantiation {arities, params} => mk_instantiation (f (arities, params))); + (fn Instantiation {arities, params} => make_instantiation (f (arities, params))); fun the_instantiation lthy = (case get_instantiation lthy of @@ -624,7 +626,7 @@ thy |> Sign.change_begin |> Proof_Context.init_global - |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params)) + |> Instantiation.put (make_instantiation ((tycos, vs, sort), params)) |> fold (Variable.declare_typ o TFree) vs |> fold (Variable.declare_names o Free o snd) params |> (Overloading.map_improvable_syntax o apfst) diff -r 0070053570c4 -r 71b416020f42 src/Pure/Isar/overloading.ML --- a/src/Pure/Isar/overloading.ML Thu Dec 18 21:10:39 2014 +0100 +++ b/src/Pure/Isar/overloading.ML Fri Dec 19 12:36:50 2014 +0100 @@ -36,7 +36,7 @@ unchecks: (term * term) list, passed: bool }; - fun init _ = { + val empty: T = { primary_constraints = [], secondary_constraints = [], improve = K NONE, @@ -45,6 +45,7 @@ unchecks = [], passed = true }; + fun init _ = empty; ); fun map_improvable_syntax f = Improvable_Syntax.map (fn {primary_constraints, diff -r 0070053570c4 -r 71b416020f42 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Dec 18 21:10:39 2014 +0100 +++ b/src/Pure/Isar/proof.ML Fri Dec 19 12:36:50 2014 +0100 @@ -1100,8 +1100,7 @@ structure Result = Proof_Data ( type T = thm option; - val empty = NONE; - fun init _ = empty; + fun init _ = NONE; ); fun the_result ctxt = diff -r 0070053570c4 -r 71b416020f42 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Thu Dec 18 21:10:39 2014 +0100 +++ b/src/Pure/Isar/toplevel.ML Fri Dec 19 12:36:50 2014 +0100 @@ -633,8 +633,7 @@ structure Result = Proof_Data ( type T = result; - val empty: T = Result_List []; - fun init _ = empty; + fun init _ = Result_List []; ); val get_result = Result.get o Proof.context_of; diff -r 0070053570c4 -r 71b416020f42 src/Pure/assumption.ML --- a/src/Pure/assumption.ML Thu Dec 18 21:10:39 2014 +0100 +++ b/src/Pure/assumption.ML Fri Dec 19 12:36:50 2014 +0100 @@ -64,11 +64,12 @@ prems: thm list}; (*prems: A |- norm_hhf A*) fun make_data (assms, prems) = Data {assms = assms, prems = prems}; +val empty_data = make_data ([], []); structure Data = Proof_Data ( type T = data; - fun init _ = make_data ([], []); + fun init _ = empty_data; ); fun map_data f = Data.map (fn Data {assms, prems} => make_data (f (assms, prems))); diff -r 0070053570c4 -r 71b416020f42 src/Pure/variable.ML --- a/src/Pure/variable.ML Thu Dec 18 21:10:39 2014 +0100 +++ b/src/Pure/variable.ML Fri Dec 19 12:36:50 2014 +0100 @@ -104,12 +104,14 @@ Data {is_body = is_body, names = names, consts = consts, bounds = bounds, fixes = fixes, binds = binds, type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints}; +val empty_data = + make_data (false, Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty, + Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty)); + structure Data = Proof_Data ( type T = data; - fun init _ = - make_data (false, Name.context, Symtab.empty, (0, []), empty_fixes, Vartab.empty, - Symtab.empty, ~1, [], (Vartab.empty, Vartab.empty)); + fun init _ = empty_data; ); fun map_data f = diff -r 0070053570c4 -r 71b416020f42 src/Tools/Code/code_runtime.ML --- a/src/Tools/Code/code_runtime.ML Thu Dec 18 21:10:39 2014 +0100 +++ b/src/Tools/Code/code_runtime.ML Fri Dec 19 12:36:50 2014 +0100 @@ -336,7 +336,8 @@ ( type T = (string list * string list) * (bool * (string * (string * string) list) lazy); - fun init _ = (([], []), (true, (Lazy.value ("", [])))); + val empty: T = (([], []), (true, (Lazy.value ("", [])))); + fun init _ = empty; ); val is_first_occ = fst o snd o Code_Antiq_Data.get;