# HG changeset patch
# User haftmann
# Date 1283346072 -7200
# Node ID cd747b068311556d13a0e64d4d41c07491f34a3a
# Parent  5d49165a192e776efa13c9d52905b1842fb3a5f0
tuned text segment

diff -r 5d49165a192e -r cd747b068311 src/HOL/HOL.thy
--- 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")