tuned;

--- a/src/HOL/Eisbach/match_method.ML	Fri Aug 05 20:17:27 2016 +0200
+++ b/src/HOL/Eisbach/match_method.ML	Fri Aug 05 20:26:13 2016 +0200
@@ -607,7 +607,7 @@
           in fold (fn seq => Seq.append (Seq.map_filter just_one seq)) thmenvs Seq.empty end);
 
     val all_matches =
-      Seq.EVERY (map proc_multi_match all_matches) ([], Envir.empty ~1);
+      Seq.EVERY (map proc_multi_match all_matches) ([], Envir.init);
   in
     all_matches
     |> Seq.map (apsnd (morphism_env morphism))

--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Aug 05 20:17:27 2016 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri Aug 05 20:26:13 2016 +0200
@@ -207,7 +207,7 @@
           |> fold (Term.add_vars o Thm.prop_of) [tha, thb]
           |> AList.group (op =)
           |> maps (fn ((s, _), T :: Ts) => map (fn T' => (Free (s, T), Free (s, T'))) Ts)
-          |> rpair (Envir.empty ~1)
+          |> rpair Envir.init
           |-> fold (Pattern.unify (Context.Proof ctxt))
           |> Envir.type_env |> Vartab.dest
           |> map (fn (x, (S, T)) => ((x, S), Thm.ctyp_of ctxt T))

--- a/src/Pure/envir.ML	Fri Aug 05 20:17:27 2016 +0200
+++ b/src/Pure/envir.ML	Fri Aug 05 20:26:13 2016 +0200
@@ -15,6 +15,7 @@
   val type_env: env -> Type.tyenv
   val is_empty: env -> bool
   val empty: int -> env
+  val init: env
   val merge: env * env -> env
   val insert_sorts: env -> sort list -> sort list
   val genvars: string -> env * typ list -> env * term list
@@ -82,6 +83,7 @@
 (* build env *)
 
 fun empty maxidx = make_env (maxidx, Vartab.empty, Vartab.empty);
+val init = empty ~1;
 
 fun merge
    (Envir {maxidx = maxidx1, tenv = tenv1, tyenv = tyenv1},

--- a/src/Pure/more_unify.ML	Fri Aug 05 20:17:27 2016 +0200
+++ b/src/Pure/more_unify.ML	Fri Aug 05 20:26:13 2016 +0200
@@ -21,7 +21,7 @@
   handle Pattern.MATCH => Seq.empty;
 
 (*General matching -- keep variables disjoint*)
-fun matchers _ [] = Seq.single (Envir.empty ~1)
+fun matchers _ [] = Seq.single Envir.init
   | matchers context pairs =
       let
         val thy = Context.theory_of context;