diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
index 0992ada..8bcafe7 100644
--- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
+++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy
@@ -405,9 +405,9 @@ types. The notation for terms and types is as follows:
 text\<open> ... where the so-called more-field \<open>\<dots>\<close> is used to 'fill-in' record-extensions.
 Schematic record types allow for simulating object-oriented features such as 
 (single-)inheritance while maintaining a compositional style of verification
-@{cite "naraschewski1998object"}: it is possible to prove a property \<^term>\<open>P (x::'a T\<close>
+@{cite "naraschewski1998object"}: it is possible to prove a property \<^term>\<open>P (a::T)\<close>
 which will remain true for all extensions (which are just instances of the
-\<^typ>\<open>'a T\<close>-type). 
+\<^typ>\<open>T\<close>-type). 
 \<close>
 
 text\<open>In \<^dof>, \<^verbatim>\<open>onto_class\<close>es and the logically equivalent  \<^verbatim>\<open>doc_class\<close>es were