# HG changeset patch
# User haftmann
# Date 1150279992 -7200
# Node ID 2b4c09941e0466395d4319bd19030af8e80785fa
# Parent  e3a03f1f54eb12e8f4d21d9df95345bac0aa5e43
slight adaptions

diff -r e3a03f1f54eb -r 2b4c09941e04 src/HOL/ex/Classpackage.thy
--- a/src/HOL/ex/Classpackage.thy	Wed Jun 14 12:12:37 2006 +0200
+++ b/src/HOL/ex/Classpackage.thy	Wed Jun 14 12:13:12 2006 +0200
@@ -314,9 +314,9 @@
   "x = ((2::nat) \<otimes> \<one> \<otimes> 3, (2::int) \<otimes> \<one> \<otimes> \<div> 3, [1::nat, 2] \<otimes> \<one> \<otimes> [1, 2, 3])"
   "y = (2 :: int, \<div> 2 :: int) \<otimes> \<one> \<otimes> (3, \<div> 3)"
 
-code_generate "op \<otimes>" "\<one>" "inv"
-code_generate x
-code_generate y
+code_generate (ml, haskell) "op \<otimes>" "\<one>" "inv"
+code_generate (ml, haskell) x
+code_generate (ml, haskell) y
 
 code_serialize ml (-)
 
diff -r e3a03f1f54eb -r 2b4c09941e04 src/HOL/ex/Codegenerator.thy
--- a/src/HOL/ex/Codegenerator.thy	Wed Jun 14 12:12:37 2006 +0200
+++ b/src/HOL/ex/Codegenerator.thy	Wed Jun 14 12:13:12 2006 +0200
@@ -14,7 +14,7 @@
   xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
   "xor p q = ((p | q) & \<not> (p & q))"
 
-code_generate (ml) xor
+code_generate (ml, haskell) xor
 
 subsection {* natural numbers *}
 
@@ -24,9 +24,9 @@
   n :: nat
   "n = 42"
 
-code_generate (ml) n
+code_generate (ml, haskell) n
 
-code_generate (ml)
+code_generate (ml, haskell)
   "0::nat" "one" n
   "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
   "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
@@ -44,7 +44,7 @@
   appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
   "appl p = (let (f, x) = p in f x)"
 
-code_generate (ml) Pair fst snd Let split swap swapp appl
+code_generate (ml, haskell) Pair fst snd Let split swap swapp appl
 
 definition
   k :: "int"
@@ -56,7 +56,7 @@
 recdef fac "measure nat"
   "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
 
-code_generate (ml)
+code_generate (ml, haskell)
   "0::int" k
   "op + :: int \<Rightarrow> int \<Rightarrow> int"
   "op - :: int \<Rightarrow> int \<Rightarrow> int"
@@ -67,11 +67,11 @@
 
 subsection {* sums *}
 
-code_generate (ml) Inl Inr
+code_generate (ml, haskell) Inl Inr
 
 subsection {* options *}
 
-code_generate (ml) None Some
+code_generate (ml, haskell) None Some
 
 subsection {* lists *}
 
@@ -81,7 +81,7 @@
   qs :: "nat list"
   "qs == rev ps"
 
-code_generate (ml) hd tl "op @" ps qs
+code_generate (ml, haskell) hd tl "op @" ps qs
 
 subsection {* mutual datatypes *}
 
@@ -98,11 +98,11 @@
   "mut2 mut2.Tip = mut2.Tip"
   "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
 
-code_generate (ml) mut1 mut2
+code_generate (ml, haskell) mut1 mut2
 
 subsection {* equalities *}
 
-code_generate (ml)
+code_generate (ml, haskell)
   "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
   "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
   "op = :: int \<Rightarrow> int \<Rightarrow> bool"
@@ -129,7 +129,7 @@
   "Codegenerator.g" "Mymod.A.f"
   "Codegenerator.h" "Mymod.A.B.f"
 
-code_generate (ml) f g h
+code_generate (ml, haskell) f g h
 
 code_serialize ml (-)