src/Pure/term_subst.ML
changeset 32738 15bb09ca0378
parent 32020 9abf5d66606e
child 35408 b48ab741683b
     1.1 --- a/src/Pure/term_subst.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/term_subst.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -157,28 +157,32 @@
     1.4  in
     1.5  
     1.6  fun instantiateT_maxidx instT ty i =
     1.7 -  let val maxidx = ref i
     1.8 +  let val maxidx = Unsynchronized.ref i
     1.9    in (instantiateT_same maxidx instT ty handle Same.SAME => ty, ! maxidx) end;
    1.10  
    1.11  fun instantiate_maxidx insts tm i =
    1.12 -  let val maxidx = ref i
    1.13 +  let val maxidx = Unsynchronized.ref i
    1.14    in (instantiate_same maxidx insts tm handle Same.SAME => tm, ! maxidx) end;
    1.15  
    1.16  fun instantiateT [] ty = ty
    1.17    | instantiateT instT ty =
    1.18 -      (instantiateT_same (ref ~1) (no_indexes1 instT) ty handle Same.SAME => ty);
    1.19 +      (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty
    1.20 +        handle Same.SAME => ty);
    1.21  
    1.22  fun instantiate ([], []) tm = tm
    1.23    | instantiate insts tm =
    1.24 -      (instantiate_same (ref ~1) (no_indexes2 insts) tm handle Same.SAME => tm);
    1.25 +      (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm
    1.26 +        handle Same.SAME => tm);
    1.27  
    1.28  fun instantiateT_option [] _ = NONE
    1.29    | instantiateT_option instT ty =
    1.30 -      (SOME (instantiateT_same (ref ~1) (no_indexes1 instT) ty) handle Same.SAME => NONE);
    1.31 +      (SOME (instantiateT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty)
    1.32 +        handle Same.SAME => NONE);
    1.33  
    1.34  fun instantiate_option ([], []) _ = NONE
    1.35    | instantiate_option insts tm =
    1.36 -      (SOME (instantiate_same (ref ~1) (no_indexes2 insts) tm) handle Same.SAME => NONE);
    1.37 +      (SOME (instantiate_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm)
    1.38 +        handle Same.SAME => NONE);
    1.39  
    1.40  end;
    1.41