src/Pure/term_subst.ML
changeset 21315 be2669fe8363
parent 21184 35baf14cfb6d
child 21607 3698319f6503
equal deleted inserted replaced
21314:6d709b9bea1a 21315:be2669fe8363
   131 
   131 
   132 fun instantiate_maxidx insts tm i =
   132 fun instantiate_maxidx insts tm i =
   133   let val maxidx = ref i
   133   let val maxidx = ref i
   134   in (instantiate_same maxidx insts tm handle SAME => tm, ! maxidx) end;
   134   in (instantiate_same maxidx insts tm handle SAME => tm, ! maxidx) end;
   135 
   135 
   136 fun instantiateT instT ty =
   136 fun instantiateT [] ty = ty
   137   instantiateT_same (ref ~1) (no_indexes1 instT) ty handle SAME => ty;
   137   | instantiateT instT ty =
       
   138       (instantiateT_same (ref ~1) (no_indexes1 instT) ty handle SAME => ty);
   138 
   139 
   139 fun instantiate insts tm =
   140 fun instantiate ([], []) tm = tm
   140   instantiate_same (ref ~1) (no_indexes2 insts) tm handle SAME => tm;
   141   | instantiate insts tm =
       
   142       (instantiate_same (ref ~1) (no_indexes2 insts) tm handle SAME => tm);
   141 
   143 
   142 fun instantiateT_option instT ty =
   144 fun instantiateT_option [] _ = NONE
   143   SOME (instantiateT_same (ref ~1) (no_indexes1 instT) ty) handle SAME => NONE;
   145   | instantiateT_option instT ty =
       
   146       (SOME (instantiateT_same (ref ~1) (no_indexes1 instT) ty) handle SAME => NONE);
   144 
   147 
   145 fun instantiate_option insts tm =
   148 fun instantiate_option ([], []) _ = NONE
   146   SOME (instantiate_same (ref ~1) (no_indexes2 insts) tm) handle SAME => NONE;
   149   | instantiate_option insts tm =
       
   150       (SOME (instantiate_same (ref ~1) (no_indexes2 insts) tm) handle SAME => NONE);
   147 
   151 
   148 end;
   152 end;
   149 
   153 
   150 
   154 
   151 (* zero var indexes *)
   155 (* zero var indexes *)