unused;

--- a/src/HOL/Eisbach/match_method.ML	Sat Dec 12 15:17:06 2015 +0100
+++ b/src/HOL/Eisbach/match_method.ML	Sat Dec 12 15:17:54 2015 +0100
@@ -312,18 +312,6 @@
     ((((Option.map prep_head x, args), params''), pat''), ctxt')
   end;
 
-fun recalculate_maxidx env =
-  let
-    val tenv = Envir.term_env env;
-    val tyenv = Envir.type_env env;
-    val max_tidx = Vartab.fold (fn (_, (_, t)) => curry Int.max (maxidx_of_term t)) tenv ~1;
-    val max_Tidx = Vartab.fold (fn (_, (_, T)) => curry Int.max (maxidx_of_typ T)) tyenv ~1;
-  in
-    Envir.Envir
-      {maxidx = Int.max (Int.max (max_tidx, max_Tidx), Envir.maxidx_of env),
-        tenv = tenv, tyenv = tyenv}
-  end
-
 fun morphism_env morphism env =
   let
     val tenv = Envir.term_env env