In the following attachment, trying open the proof obligation thm1/S-THM for "Theory" resulting in exception "java.lang.IllegalArgumentException: Trying to register an existing name with a different type" for RbP0.getPossibleApplications().
For the user the symtom is that the operator "cmp" (which should be redden for "definition expansion") is not redden.
This is a bug reported by J-R. Abrial via email.
The matching facilities has been reimplemented using ISpecialization which is the proper way for instantiate types in Rodin 3.x. The fix will be available in the next release of the Theory plug-in
This bug can't be reproduced with the latest version of the Theory plug-in: it is possible to open and prove thm1/S-THM without issue.
It must have been fixed at some point, but the issue was not closed at the time.