src/Pure/pattern.ML
changeset 12826 dfb214fa310b
parent 12817 fcbb6ad5c790
child 12980 8f717cbd4e44
     1.1 --- a/src/Pure/pattern.ML	Mon Jan 21 14:47:55 2002 +0100
     1.2 +++ b/src/Pure/pattern.ML	Mon Jan 21 14:48:11 2002 +0100
     1.3 @@ -451,6 +451,6 @@
     1.4            end
     1.5        | rew2 _ = None
     1.6  
     1.7 -  in if_none (timeap_msg "FIXME: rewrite_term" rew1 tm) tm end;
     1.8 +  in if_none (rew1 tm) tm end;
     1.9  
    1.10  end;