Lars noticed an anomaly and Gerwin tracked it down: Command find_consts searches only for `visible' constants. Those defined by primrec and fun are visible, but those defined by inductive(_set) are concealed. It seems that the latter should be visible, too, right? If so, can somebody close to "inductive" fix that? Tobias