# HG changeset patch
# User haftmann
# Date 1288790045 -3600
# Node ID 090dac52cfd78181f1757fa6a6dee670503cf3a9
# Parent  1ef7ee8dd165b19646736b47d03f5610599ea560
SMLdummy target

diff -r 1ef7ee8dd165 -r 090dac52cfd7 doc-src/Codegen/Thy/Adaptation.thy
--- a/doc-src/Codegen/Thy/Adaptation.thy	Wed Nov 03 14:14:05 2010 +0100
+++ b/doc-src/Codegen/Thy/Adaptation.thy	Wed Nov 03 14:14:05 2010 +0100
@@ -2,7 +2,8 @@
 imports Setup
 begin
 
-setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", K I)) *}
+setup %invisible {* Code_Target.extend_target ("\<SML>", ("SML", K I))
+  #> Code_Target.extend_target ("\<SMLdummy>", ("Haskell", K I)) *}
 
 section {* Adaptation to target languages \label{sec:adaptation} *}
 
@@ -235,7 +236,7 @@
   @{command_def "code_reserved"} command:
 *}
 
-code_reserved %quote "\<SML>" bool true false andalso
+code_reserved %quote "\<SMLdummy>" bool true false andalso
 
 text {*
   \noindent Next, we try to map HOL pairs to SML pairs, using the
diff -r 1ef7ee8dd165 -r 090dac52cfd7 doc-src/Codegen/Thy/document/Adaptation.tex
--- a/doc-src/Codegen/Thy/document/Adaptation.tex	Wed Nov 03 14:14:05 2010 +0100
+++ b/doc-src/Codegen/Thy/document/Adaptation.tex	Wed Nov 03 14:14:05 2010 +0100
@@ -26,7 +26,8 @@
 %
 \isataginvisible
 \isacommand{setup}\isamarkupfalse%
-\ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
+\ {\isacharverbatimopen}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSML}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}SML{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\isanewline
+\ \ {\isacharhash}{\isachargreater}\ Code{\isacharunderscore}Target{\isachardot}extend{\isacharunderscore}target\ {\isacharparenleft}{\isachardoublequote}{\isasymSMLdummy}{\isachardoublequote}{\isacharcomma}\ {\isacharparenleft}{\isachardoublequote}Haskell{\isachardoublequote}{\isacharcomma}\ K\ I{\isacharparenright}{\isacharparenright}\ {\isacharverbatimclose}%
 \endisataginvisible
 {\isafoldinvisible}%
 %
@@ -420,7 +421,7 @@
 %
 \isatagquote
 \isacommand{code{\isacharunderscore}reserved}\isamarkupfalse%
-\ {\isachardoublequoteopen}{\isasymSML}{\isachardoublequoteclose}\ bool\ true\ false\ andalso%
+\ {\isachardoublequoteopen}{\isasymSMLdummy}{\isachardoublequoteclose}\ bool\ true\ false\ andalso%
 \endisatagquote
 {\isafoldquote}%
 %
diff -r 1ef7ee8dd165 -r 090dac52cfd7 doc-src/Codegen/style.sty
--- a/doc-src/Codegen/style.sty	Wed Nov 03 14:14:05 2010 +0100
+++ b/doc-src/Codegen/style.sty	Wed Nov 03 14:14:05 2010 +0100
@@ -45,6 +45,7 @@
 
 %% a trick
 \newcommand{\isasymSML}{SML}
+\newcommand{\isasymSMLdummy}{SML}
 
 %% presentation
 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}