use command_def
authorhaftmann
Wed, 18 Aug 2010 10:07:56 +0200
changeset 38506 03d767575713
parent 38505 2f8699695cf6
child 38507 06728ef076a7
use command_def
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