# HG changeset patch
# User haftmann
# Date 1162303092 -3600
# Node ID 9b7d35ca1eef525feea4c283fd5ce678dabe8b97
# Parent  8648b5dd6a8771b3926286bf34946f13f1e85c86
adapted to new serializer syntax

diff -r 8648b5dd6a87 -r 9b7d35ca1eef NEWS
--- a/NEWS	Tue Oct 31 09:29:18 2006 +0100
+++ b/NEWS	Tue Oct 31 14:58:12 2006 +0100
@@ -52,7 +52,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 8648b5dd6a87 -r 9b7d35ca1eef src/HOL/Extraction/QuotRem.thy
--- a/src/HOL/Extraction/QuotRem.thy	Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/Extraction/QuotRem.thy	Tue Oct 31 14:58:12 2006 +0100
@@ -49,6 +49,6 @@
 contains
   test = "division 9 2"
 
-code_gen division (SML -)
+code_gen division (SML *)
 
 end
diff -r 8648b5dd6a87 -r 9b7d35ca1eef src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy	Tue Oct 31 14:58:12 2006 +0100
@@ -584,7 +584,7 @@
 *}
 
 code_gen
-  type_NF (SML -) (SML _)
+  type_NF (SML *)
 
 ML {*
 structure Norm = ROOT.WeakNorm;
diff -r 8648b5dd6a87 -r 9b7d35ca1eef src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy	Tue Oct 31 14:58:12 2006 +0100
@@ -133,8 +133,8 @@
   (Haskell "0")
 
 code_const "Suc"
-  (SML "IntInf.+ (__, 1)")
-  (Haskell "!(__ + 1)")
+  (SML "IntInf.+ ((_), 1)")
+  (Haskell "!((_) + 1)")
 
 setup {*
   CodegenData.del_datatype "nat"
diff -r 8648b5dd6a87 -r 9b7d35ca1eef src/HOL/Library/ExecutableRat.thy
--- a/src/HOL/Library/ExecutableRat.thy	Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/Library/ExecutableRat.thy	Tue Oct 31 14:58:12 2006 +0100
@@ -143,7 +143,7 @@
   "inverse \<Colon> rat \<Rightarrow> rat"
   "op \<le> \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
    "Code_Generator.eq \<Colon> rat \<Rightarrow> rat \<Rightarrow> bool"
-  (SML -)
+  (SML *)
 
 
 section {* type serializations *}
diff -r 8648b5dd6a87 -r 9b7d35ca1eef src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Tue Oct 31 14:58:12 2006 +0100
@@ -285,7 +285,7 @@
   Bex \<equiv> Blex
 
 code_gen "{}" insert "op \<union>" "op \<inter>" "op - \<Colon> 'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
-  image Union Inter UNION INTER Ball Bex (SML -)
+  image Union Inter UNION INTER Ball Bex (SML *)
 
 
 subsection {* type serializations *}
diff -r 8648b5dd6a87 -r 9b7d35ca1eef src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/ex/Classpackage.thy	Tue Oct 31 14:58:12 2006 +0100
@@ -323,7 +323,7 @@
 code_gen X Y (SML) (Haskell)
 code_gen x1 x2 y2 (SML) (Haskell)
 
-code_gen (SML -)
+code_gen (SML *)
 code_gen (Haskell -)
 
 end
diff -r 8648b5dd6a87 -r 9b7d35ca1eef src/HOL/ex/CodeCollections.thy
--- a/src/HOL/ex/CodeCollections.thy	Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/ex/CodeCollections.thy	Tue Oct 31 14:58:12 2006 +0100
@@ -406,7 +406,7 @@
 code_gen test1
 code_gen test2
 
-code_gen (SML -)
+code_gen (SML *)
 code_gen (Haskell -)
 
 end
\ No newline at end of file
diff -r 8648b5dd6a87 -r 9b7d35ca1eef src/HOL/ex/CodeRandom.thy
--- a/src/HOL/ex/CodeRandom.thy	Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/ex/CodeRandom.thy	Tue Oct 31 14:58:12 2006 +0100
@@ -182,6 +182,6 @@
   (SML "case _ (Random.seed ()) of (x, '_) => x")
 
 code_gen select select_weight
-  (SML -)
+  (SML *)
 
 end
\ No newline at end of file
diff -r 8648b5dd6a87 -r 9b7d35ca1eef src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Tue Oct 31 09:29:18 2006 +0100
+++ b/src/HOL/ex/Codegenerator.thy	Tue Oct 31 14:58:12 2006 +0100
@@ -5,7 +5,7 @@
 header {* Test and Examples for code generator *}
 
 theory Codegenerator
-imports Main Records
+imports Main (*"~/projects/codegen/thy/CodegenSetup"*) Records
 begin
 
 subsection {* booleans *}
@@ -197,7 +197,7 @@
   "Code_Generator.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   "Code_Generator.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
 
-code_gen (SML -)
+code_gen (SML *)
 code_gen (Haskell -)
 
 end
\ No newline at end of file