# HG changeset patch
# User haftmann
# Date 1671268323 -3600
# Node ID 2afbd514b654516c097c75c88ae7a5a6f1e4384e
# Parent  e60fd6257abe234ce53ac542e3d1a4cd29df00ec
Typo.

diff -r e60fd6257abe -r 2afbd514b654 src/Doc/Codegen/Computations.thy
--- a/src/Doc/Codegen/Computations.thy	Fri Dec 16 20:14:41 2022 +0100
+++ b/src/Doc/Codegen/Computations.thy	Sat Dec 17 10:12:03 2022 +0100
@@ -241,7 +241,7 @@
 subsection \<open>Pitfalls concerning input terms\<close>
 
 text \<open>
-    \<^descr> \<open>No polymorphims.\<close> Input terms must be monomorphic: compilation
+    \<^descr> \<open>No polymorphism.\<close> Input terms must be monomorphic: compilation
       to ML requires dedicated choice of monomorphic types.
 
     \<^descr> \<open>No abstractions.\<close> Only constants and applications are admissible