# HG changeset patch
# User wenzelm
# Date 1449929874 -3600
# Node ID afdbf76a0ded3b3bfdbd30505cfb91389d27589a
# Parent  2111b95e692f1f58f9a907d4c275d13fbb058c09
unused;

diff -r 2111b95e692f -r afdbf76a0ded src/HOL/Eisbach/match_method.ML
--- 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