Does anyboy remember why fconv_rule is called like this? After peeking into the HOL Light sources I've got the impression that this function is usually called conv_rule. (Conversions have become popular recently so it might be a good point to sort this out now.) Makarius