Convert month name to month number faster

[wiso]

I'm optimizing the inner most loop of my script. I need to convert month 
name to month number. I'm using python 2.6 on linux x64.


month_dict = {"Jan":1,"Feb":2,"Mar":3,"Apr":4, "May":5, "Jun":6,
	   "Jul":7,"Aug":8,"Sep":9,"Oct":10,"Nov":11,"Dec":12}

def to_dict(name):
  return month_dict[name]

def to_if(name):
    if name == "Jan": return 1
    elif name == "Feb": return 2
    elif name == "Mar": return 3
    elif name == "Apr": return 4
    elif name == "May": return 5
    elif name == "Jun": return 6
    elif name == "Jul": return 7
    elif name == "Aug": return 8
    elif name == "Sep": return 9
    elif name == "Oct": return 10
    elif name == "Nov": return 11
    elif name == "Dec": return 12
    else: raise ValueError

import random
l = [random.choice(month_dict.keys()) for _ in range(1000000)]

from time import time
t = time(); xxx=map(to_dict,l); print time() - t # 0.5
t = time(); xxx=map(to_if,l); print time() - t   # 1.0


is there a faster solution? Maybe something with str.translate?

The problem is a little different because I don't read random data, but 
sorted data. For example:

l = [x for x in 
("Jan","Feb","Mar","Apr","May","Jun","Jul","Aug","Sep","Oct","Nov","Dec") 
for _ in range(1000)] # ["Jan","Jan", ..., "Feb", "Feb", ...]

so maybe the to_if approach will be faster if I write the case in the best 
order. Look:

l = ["Jan"] * 1000000 # to_if is in the best order for "Jan"
t = time(); xxx=map(to_dict,l); print time() - t # 0.5
t = time(); xxx=map(to_if,l); print time() - t # 0.5