clarified identity of theory data: avoid accidental pointer_eq, use equality on unique serial instead;