diff -r a76f457b6d86 -r 35baf14cfb6d src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Sun Nov 05 21:44:37 2006 +0100
+++ b/src/Pure/term_subst.ML	Sun Nov 05 21:44:39 2006 +0100
@@ -81,17 +81,16 @@
 
 local
 
-val maxidx = ref ~1;
-fun maxify i = if i > ! maxidx then maxidx := i else ();
-
 fun no_index (x, y) = (x, (y, ~1));
 fun no_indexes1 inst = map no_index inst;
 fun no_indexes2 (inst1, inst2) = (map no_index inst1, map no_index inst2);
 
 exception SAME;
 
-fun instantiateT_same instT ty =
+fun instantiateT_same maxidx instT ty =
   let
+    fun maxify i = if i > ! maxidx then maxidx := i else ();
+
     fun subst_typ (Type (a, Ts)) = Type (a, subst_typs Ts)
       | subst_typ (TVar ((a, i), S)) =
           (case AList.lookup Term.eq_tvar instT ((a, i), S) of
@@ -104,9 +103,11 @@
       | subst_typs [] = raise SAME;
   in subst_typ ty end;
 
-fun instantiate_same (instT, inst) tm =
+fun instantiate_same maxidx (instT, inst) tm =
   let
-    val substT = instantiateT_same instT;
+    fun maxify i = if i > ! maxidx then maxidx := i else ();
+
+    val substT = instantiateT_same maxidx instT;
     fun subst (Const (c, T)) = Const (c, substT T)
       | subst (Free (x, T)) = Free (x, substT T)
       | subst (Var ((x, i), T)) =
@@ -125,19 +126,24 @@
 in
 
 fun instantiateT_maxidx instT ty i =
-  (maxidx := i; (instantiateT_same instT ty handle SAME => ty, ! maxidx));
+  let val maxidx = ref i
+  in (instantiateT_same maxidx instT ty handle SAME => ty, ! maxidx) end;
 
 fun instantiate_maxidx insts tm i =
-  (maxidx := i; (instantiate_same insts tm handle SAME => tm, ! maxidx));
+  let val maxidx = ref i
+  in (instantiate_same maxidx insts tm handle SAME => tm, ! maxidx) end;
 
-fun instantiateT instT ty = instantiateT_same (no_indexes1 instT) ty handle SAME => ty;
-fun instantiate insts tm = instantiate_same (no_indexes2 insts) tm handle SAME => tm;
+fun instantiateT instT ty =
+  instantiateT_same (ref ~1) (no_indexes1 instT) ty handle SAME => ty;
+
+fun instantiate insts tm =
+  instantiate_same (ref ~1) (no_indexes2 insts) tm handle SAME => tm;
 
 fun instantiateT_option instT ty =
-  SOME (instantiateT_same (no_indexes1 instT) ty) handle SAME => NONE;
+  SOME (instantiateT_same (ref ~1) (no_indexes1 instT) ty) handle SAME => NONE;
 
 fun instantiate_option insts tm =
-  SOME (instantiate_same (no_indexes2 insts) tm) handle SAME => NONE;
+  SOME (instantiate_same (ref ~1) (no_indexes2 insts) tm) handle SAME => NONE;
 
 end;