--- a/src/HOL/HOL.thy Wed Sep 01 12:01:44 2010 +0200 +++ b/src/HOL/HOL.thy Wed Sep 01 15:01:12 2010 +0200 @@ -1896,9 +1896,10 @@ code_abort undefined + subsubsection {* Generic code generator target languages *} -text {* type bool *} +text {* type @{typ bool} *} code_type bool (SML "bool")