[isabelle-dev] Rat.normalize

[Makarius]

Theory Rat (formerly Rational) has a function called "normalize".  This is 
a rather generic name for main HOL -- today I've seen a user theory where 
it has caused a clash.  (It was easy to fix by using an explicit binding 
in the 'definition' command in question, but it is confusing nonetheless.)

Is there a better name for Rat.normalize?  Alternatively, one could just 
use hide_const (open) in theory Rat as is now done for many other things 
in main HOL.


 	Makarius