# HG changeset patch
# User haftmann
# Date 1282118876 -7200
# Node ID 03d767575713e15c27f6570ba932a52d5844a2ed
# Parent  2f8699695cf676025c2963dca97563b5a1e33bd9
use command_def

diff -r 2f8699695cf6 -r 03d767575713 doc-src/Codegen/Thy/Adaptation.thy
--- a/doc-src/Codegen/Thy/Adaptation.thy	Wed Aug 18 09:55:00 2010 +0200
+++ b/doc-src/Codegen/Thy/Adaptation.thy	Wed Aug 18 10:07:56 2010 +0200
@@ -307,7 +307,7 @@
 text {*
   \noindent The code generator would produce an additional instance,
   which of course is rejected by the @{text Haskell} compiler.  To
-  suppress this additional instance, use @{text "code_instance"}:
+  suppress this additional instance, use @{command_def "code_instance"}:
 *}
 
 code_instance %quotett bar :: eq