# HG changeset patch
# User haftmann
# Date 1164631350 -3600
# Node ID 54cc492d80a9f05e8af45d2d8ba2ac79433c0b11
# Parent  a9ceeb182cfcb7d5513ecf05f92f6b0fd3900011
adjusted syntax for internal code generation

diff -r a9ceeb182cfc -r 54cc492d80a9 NEWS
--- a/NEWS	Mon Nov 27 12:12:18 2006 +0100
+++ b/NEWS	Mon Nov 27 13:42:30 2006 +0100
@@ -63,7 +63,7 @@
 code for ML and Haskell (including "class"es). A short usage sketch:
 
     internal compilation:
-        code_gen <list of constants (term syntax)> (SML *)
+        code_gen <list of constants (term syntax)> (SML #)
     writing SML code to a file:
         code_gen <list of constants (term syntax)> (SML <filename>)
     writing Haskell code to a bunch of files:
diff -r a9ceeb182cfc -r 54cc492d80a9 doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy
--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Nov 27 12:12:18 2006 +0100
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy	Mon Nov 27 13:42:30 2006 +0100
@@ -153,7 +153,7 @@
   This executable specification is now turned to SML code:
 *}
 
-code_gen fac (*<*)(SML *)(*>*)(SML "examples/fac.ML")
+code_gen fac (*<*)(SML #)(*>*)(SML "examples/fac.ML")
 
 text {*
   The @{text "\<CODEGEN>"} command takes a space-separated list of
@@ -269,7 +269,7 @@
   "pick ((k, v)#xs) n = (if n < k then v else pick xs (n - k))"
   by simp
 
-code_gen pick (*<*)(SML *)(*>*)(SML "examples/pick1.ML")
+code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick1.ML")
 
 text {*
   This theorem is now added to the function equation table:
@@ -282,7 +282,7 @@
 
 lemmas [code nofunc] = pick.simps 
 
-code_gen pick (*<*)(SML *)(*>*)(SML "examples/pick2.ML")
+code_gen pick (*<*)(SML #)(*>*)(SML "examples/pick2.ML")
 
 text {*
   \lstsml{Thy/examples/pick2.ML}
@@ -298,7 +298,7 @@
   "fac n = (case n of 0 \<Rightarrow> 1 | Suc m \<Rightarrow> n * fac m)"
   by (cases n) simp_all
 
-code_gen fac (*<*)(SML *)(*>*)(SML "examples/fac_case.ML")
+code_gen fac (*<*)(SML #)(*>*)(SML "examples/fac_case.ML")
 
 text {*
   \lstsml{Thy/examples/fac_case.ML}
@@ -377,7 +377,7 @@
   The whole code in SML with explicit dictionary passing:
 *}
 
-code_gen dummy (*<*)(SML *)(*>*)(SML "examples/class.ML")
+code_gen dummy (*<*)(SML #)(*>*)(SML "examples/class.ML")
 
 text {*
   \lstsml{Thy/examples/class.ML}
@@ -557,7 +557,7 @@
   (SML and and and)
 (*>*)
 
-code_gen in_interval (*<*)(SML *)(*>*)(SML "examples/bool_literal.ML")
+code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_literal.ML")
 
 text {*
   \lstsml{Thy/examples/bool_literal.ML}
@@ -600,7 +600,7 @@
   After this setup, code looks quite more readable:
 *}
 
-code_gen in_interval (*<*)(SML *)(*>*)(SML "examples/bool_mlbool.ML")
+code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_mlbool.ML")
 
 text {*
   \lstsml{Thy/examples/bool_mlbool.ML}
@@ -616,7 +616,7 @@
 code_const %tt "op \<and>"
   (SML infixl 1 "andalso")
 
-code_gen in_interval (*<*)(SML *)(*>*)(SML "examples/bool_infix.ML")
+code_gen in_interval (*<*)(SML #)(*>*)(SML "examples/bool_infix.ML")
 
 text {*
   \lstsml{Thy/examples/bool_infix.ML}
@@ -675,7 +675,7 @@
     and "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
   (SML "IntInf.+ (_, _)" and "IntInf.* (_, _)")
 
-code_gen double_inc (*<*)(SML *)(*>*)(SML "examples/integers.ML")
+code_gen double_inc (*<*)(SML #)(*>*)(SML "examples/integers.ML")
 
 text {*
   resulting in:
@@ -727,7 +727,7 @@
   performs an explicit equality check.
 *}
 
-code_gen collect_duplicates (*<*)(SML *)(*>*)(SML "examples/collect_duplicates.ML")
+code_gen collect_duplicates (*<*)(SML #)(*>*)(SML "examples/collect_duplicates.ML")
 
 text {*
   \lstsml{Thy/examples/collect_duplicates.ML}
@@ -803,7 +803,7 @@
   Then everything goes fine:
 *}
 
-code_gen lookup (*<*)(SML *)(*>*)(SML "examples/lookup.ML")
+code_gen lookup (*<*)(SML #)(*>*)(SML "examples/lookup.ML")
 
 text {*
   \lstsml{Thy/examples/lookup.ML}
@@ -856,7 +856,7 @@
 *}
 
 code_gen "op \<le> \<Colon> 'a\<Colon>{eq, ord} \<times> 'b\<Colon>{eq, ord} \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
-  (*<*)(SML *)(*>*)(SML "examples/lexicographic.ML")
+  (*<*)(SML #)(*>*)(SML "examples/lexicographic.ML")
 
 text {*
   \lstsml{Thy/examples/lexicographic.ML}
@@ -960,7 +960,7 @@
 lemma [code func]:
   "insert = insert" ..
 
-code_gen dummy_set foobar_set (*<*)(SML *)(*>*)(SML "examples/dirty_set.ML")
+code_gen dummy_set foobar_set (*<*)(SML #)(*>*)(SML "examples/dirty_set.ML")
 
 text {*
   \lstsml{Thy/examples/dirty_set.ML}
@@ -1087,7 +1087,7 @@
 declare dummy_option.simps [code func]
 (*>*)
 
-code_gen dummy_option (*<*)(SML *)(*>*)(SML "examples/arbitrary.ML")
+code_gen dummy_option (*<*)(SML #)(*>*)(SML "examples/arbitrary.ML")
 
 text {*
   \lstsml{Thy/examples/arbitrary.ML}
diff -r a9ceeb182cfc -r 54cc492d80a9 src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Mon Nov 27 12:12:18 2006 +0100
+++ b/src/HOL/Extraction/Higman.thy	Mon Nov 27 13:42:30 2006 +0100
@@ -337,7 +337,7 @@
 end;
 *}
 
-code_gen good_prefix (SML *)
+code_gen good_prefix (SML #)
 
 ML {*
 local
diff -r a9ceeb182cfc -r 54cc492d80a9 src/HOL/Extraction/Pigeonhole.thy
--- a/src/HOL/Extraction/Pigeonhole.thy	Mon Nov 27 12:12:18 2006 +0100
+++ b/src/HOL/Extraction/Pigeonhole.thy	Mon Nov 27 13:42:30 2006 +0100
@@ -316,7 +316,7 @@
 definition
   "test' n = pigeonhole_slow n (\<lambda>m. m - 1)"
 
-code_gen test test' "op !" (SML *)
+code_gen test test' "op !" (SML #)
 
 ML "timeit (fn () => ROOT.Pigeonhole.test 10)"
 ML "timeit (fn () => ROOT.Pigeonhole.test' 10)"
diff -r a9ceeb182cfc -r 54cc492d80a9 src/HOL/Extraction/QuotRem.thy
--- a/src/HOL/Extraction/QuotRem.thy	Mon Nov 27 12:12:18 2006 +0100
+++ b/src/HOL/Extraction/QuotRem.thy	Mon Nov 27 13:42:30 2006 +0100
@@ -49,6 +49,6 @@
 contains
   test = "division 9 2"
 
-code_gen division (SML *)
+code_gen division (SML #)
 
 end
diff -r a9ceeb182cfc -r 54cc492d80a9 src/HOL/Library/ExecutableRat.thy
--- a/src/HOL/Library/ExecutableRat.thy	Mon Nov 27 12:12:18 2006 +0100
+++ b/src/HOL/Library/ExecutableRat.thy	Mon Nov 27 13:42:30 2006 +0100
@@ -137,7 +137,7 @@
   "inverse \<Colon> rat \<Rightarrow> rat"
   "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
   "op = \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
-  (SML *)
+  (SML #)
 
 
 section {* type serializations *}
diff -r a9ceeb182cfc -r 54cc492d80a9 src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Mon Nov 27 12:12:18 2006 +0100
+++ b/src/HOL/ex/Classpackage.thy	Mon Nov 27 13:42:30 2006 +0100
@@ -320,7 +320,7 @@
 definition "y2 = Y (1::int) 2 3"
 
 code_gen "op \<otimes>" \<one> inv
-code_gen X Y (SML *) (Haskell -)
-code_gen x1 x2 y2 (SML *) (Haskell -)
+code_gen X Y (SML #) (Haskell -)
+code_gen x1 x2 y2 (SML #) (Haskell -)
 
 end
diff -r a9ceeb182cfc -r 54cc492d80a9 src/HOL/ex/CodeCollections.thy
--- a/src/HOL/ex/CodeCollections.thy	Mon Nov 27 12:12:18 2006 +0100
+++ b/src/HOL/ex/CodeCollections.thy	Mon Nov 27 13:42:30 2006 +0100
@@ -198,7 +198,7 @@
 
 code_gen test3
 
-code_gen (SML *)
+code_gen (SML #)
 code_gen (Haskell -)
 
 end
\ No newline at end of file
diff -r a9ceeb182cfc -r 54cc492d80a9 src/HOL/ex/CodeRandom.thy
--- a/src/HOL/ex/CodeRandom.thy	Mon Nov 27 12:12:18 2006 +0100
+++ b/src/HOL/ex/CodeRandom.thy	Mon Nov 27 13:42:30 2006 +0100
@@ -187,7 +187,7 @@
   (SML "case _ (Random.seed ()) of (x, '_) => x")
 
 code_gen select select_weight
-  (SML *)
+  (SML #)
 
 code_gen (SML -)
 
diff -r a9ceeb182cfc -r 54cc492d80a9 src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Mon Nov 27 12:12:18 2006 +0100
+++ b/src/HOL/ex/Codegenerator.thy	Mon Nov 27 13:42:30 2006 +0100
@@ -188,6 +188,6 @@
   "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   "op = :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
 
-code_gen (SML *) (Haskell -)
+code_gen (SML #) (Haskell -)
 
 end
\ No newline at end of file