# HG changeset patch
# User haftmann
# Date 1138605656 -3600
# Node ID 9502ce541f01590942a755eca0d01a4aa79d80f8
# Parent  92ef83e5eaea28521cf605aab6b6812c27846d18
adaptions to codegen_package

diff -r 92ef83e5eaea -r 9502ce541f01 src/HOL/Library/EfficientNat.thy
--- a/src/HOL/Library/EfficientNat.thy	Mon Jan 30 08:20:06 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy	Mon Jan 30 08:20:56 2006 +0100
@@ -51,26 +51,26 @@
 *}
   int ("(_)")
 
-(* code_syntax_tyco nat
-  ml (target_atom "InfInt.int")
+code_primconst nat
+ml {*
+fun nat i = if i < 0 then 0 : IntInf.int else i;
+*}
+haskell {*
+nat i = if i < 0 then 0 else i
+*}
+
+code_syntax_tyco nat
+  ml (target_atom "IntInf.int")
   haskell (target_atom "Integer")
 
 code_syntax_const 0 :: nat
-  ml ("0 : InfInt.int")
+  ml (target_atom "(0:IntInf.int)")
   haskell (target_atom "0")
 
 code_syntax_const Suc
   ml (infixl 8 "_ + 1")
   haskell (infixl 6 "_ + 1")
 
-code_primconst nat
-ml {*
-fun nat i = if i < 0 then 0 else i;
-*}
-haskell {*
-nat i = if i < 0 then 0 else i
-*} *)
-
 text {*
 Case analysis on natural numbers is rephrased using a conditional
 expression:
diff -r 92ef83e5eaea -r 9502ce541f01 src/HOL/Library/ExecutableSet.thy
--- a/src/HOL/Library/ExecutableSet.thy	Mon Jan 30 08:20:06 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy	Mon Jan 30 08:20:56 2006 +0100
@@ -62,7 +62,7 @@
 fun Ball S P = Library.forall P S;
 *}
 
-code_generate ("op mem")
+code_generate "op mem"
 
 code_primconst "insert"
   depending_on ("List.const.member")
@@ -77,8 +77,9 @@
 *}
 
 code_primconst "op Un"
-  depending_on ("List.const.insert")
+  depending_on ("Set.const.insert")
 ml {*
+nonfix union;
 fun union xs [] = xs
   | union [] ys = ys
   | union (x::xs) ys = union xs (insert x ys);
@@ -92,6 +93,7 @@
 code_primconst "op Int"
   depending_on ("List.const.member")
 ml {*
+nonfix inter;
 fun inter [] ys = []
   | inter (x::xs) ys =
       if List.member x ys
@@ -139,32 +141,32 @@
   img xs (y:ys) = img (insert (f y) xs) ys;
 *}
 
+code_primconst "INTER"
+  depending_on ("Set.const.inter")
+ml {*
+fun INTER [] f = []
+  | INTER (x::xs) f = inter (f x) (INTER xs f);
+*}
+haskell {*
+INTER [] f = []
+INTER (x:xs) f = inter (f x) (INTER xs f);
+*}
+
 code_primconst "UNION"
-  depending_on ("List.const.union")
+  depending_on ("Set.const.union")
 ml {*
 fun UNION [] f = []
-  | UNION (x::xs) f = union (f x) (UNION xs);
+  | UNION (x::xs) f = union (f x) (UNION xs f);
 *}
 haskell {*
 UNION [] f = []
-UNION (x:xs) f = union (f x) (UNION xs);
-*}
-
-code_primconst "INTER"
-  depending_on ("List.const.inter")
-ml {*
-fun INTER [] f = []
-  | INTER (x::xs) f = inter (f x) (INTER xs);
-*}
-haskell {*
-INTER [] f = []
-INTER (x:xs) f = inter (f x) (INTER xs);
+UNION (x:xs) f = union (f x) (UNION xs f);
 *}
 
 code_primconst "Ball"
 ml {*
 fun Ball [] f = true
-  | Ball (x::xs) f = f x andalso Ball f xs;
+  | Ball (x::xs) f = f x andalso Ball xs f;
 *}
 haskell {*
 Ball = all . flip
@@ -173,7 +175,7 @@
 code_primconst "Bex"
 ml {*
 fun Bex [] f = false
-  | Bex (x::xs) f = f x orelse Bex f xs;
+  | Bex (x::xs) f = f x orelse Bex xs f;
 *}
 haskell {*
 Ball = any . flip
diff -r 92ef83e5eaea -r 9502ce541f01 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Mon Jan 30 08:20:06 2006 +0100
+++ b/src/HOL/Orderings.thy	Mon Jan 30 08:20:56 2006 +0100
@@ -706,7 +706,7 @@
 subsection {* Code generator setup *}
 
 code_alias
-  "op <=" "Orderings.op_le"
-  "op <" "Orderings.op_lt"
+  "op <=" "IntDef.op_le"
+  "op <" "IntDef.op_lt"
 
 end
diff -r 92ef83e5eaea -r 9502ce541f01 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Jan 30 08:20:06 2006 +0100
+++ b/src/HOL/Set.thy	Mon Jan 30 08:20:56 2006 +0100
@@ -2244,4 +2244,10 @@
   ord_eq_less_trans
   trans
 
+subsection {* Code generator setup *}
+
+code_alias
+  "op Int" "Set.inter"
+  "op Un" "Set.union"
+
 end