src/Pure/pattern.ML
changeset 12826 dfb214fa310b
parent 12817 fcbb6ad5c790
child 12980 8f717cbd4e44
equal deleted inserted replaced
12825:f1f7964ed05c 12826:dfb214fa310b
   449               Some tm'' => Some (abs tm'')
   449               Some tm'' => Some (abs tm'')
   450             | None => None)
   450             | None => None)
   451           end
   451           end
   452       | rew2 _ = None
   452       | rew2 _ = None
   453 
   453 
   454   in if_none (timeap_msg "FIXME: rewrite_term" rew1 tm) tm end;
   454   in if_none (rew1 tm) tm end;
   455 
   455 
   456 end;
   456 end;