src/Pure/variable.ML
changeset 33957 e9afca2118d4
parent 33955 fff6f11b1f09
child 36603 d5d6111761a6
equal deleted inserted replaced
33956:6f549f5e7066 33957:e9afca2118d4
   343   let
   343   let
   344     val declared_outer = is_declared outer;
   344     val declared_outer = is_declared outer;
   345     val fixes_inner = fixes_of inner;
   345     val fixes_inner = fixes_of inner;
   346     val fixes_outer = fixes_of outer;
   346     val fixes_outer = fixes_of outer;
   347 
   347 
   348     val gen_fixes = map #2 ((uncurry take) (length fixes_inner - length fixes_outer, fixes_inner));
   348     val gen_fixes = map #2 (take (length fixes_inner - length fixes_outer) fixes_inner);
   349     val still_fixed = not o member (op =) gen_fixes;
   349     val still_fixed = not o member (op =) gen_fixes;
   350 
   350 
   351     val type_occs_inner = type_occs_of inner;
   351     val type_occs_inner = type_occs_of inner;
   352     fun gen_fixesT ts =
   352     fun gen_fixesT ts =
   353       Symtab.fold (fn (a, xs) =>
   353       Symtab.fold (fn (a, xs) =>