tuned;

--- 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)

--- 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,

--- 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 =

--- 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;

--- 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)));

--- 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 =

--- 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;