# HG changeset patch
# User haftmann
# Date 1174568610 -3600
# Node ID 68c8a8390e16f596708e1f399e66d34ebab13f58
# Parent  62cdd4b3e96bfc0f5e744521f6ddcc8317c65bc6
fixed code generator setup

diff -r 62cdd4b3e96b -r 68c8a8390e16 src/HOL/Code_Generator.thy
--- a/src/HOL/Code_Generator.thy	Thu Mar 22 13:36:57 2007 +0100
+++ b/src/HOL/Code_Generator.thy	Thu Mar 22 14:03:30 2007 +0100
@@ -175,8 +175,8 @@
 text {* code generation for undefined as exception *}
 
 code_const undefined
-  (SML "(raise Fail \"undefined\")")
-  (OCaml "(failwith \"undefined\")")
+  (SML "raise/ Fail/ \"undefined\"")
+  (OCaml "failwith/ \"undefined\"")
   (Haskell "error/ \"undefined\"")
 
 code_reserved SML Fail
diff -r 62cdd4b3e96b -r 68c8a8390e16 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Thu Mar 22 13:36:57 2007 +0100
+++ b/src/HOL/Lambda/WeakNorm.thy	Thu Mar 22 14:03:30 2007 +0100
@@ -18,9 +18,7 @@
 
 definition
   listall :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool" where
-  "listall P xs == (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
-
-declare listall_def [extraction_expand]
+  [extraction_expand]: "listall P xs \<equiv> (\<forall>i. i < length xs \<longrightarrow> P (xs ! i))"
 
 theorem listall_nil: "listall P []"
   by (simp add: listall_def)
@@ -573,19 +571,21 @@
 The same story again for code next generation.
 *}
 
+setup {*
+  CodegenSerializer.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
+*}
+
 code_gen
-  type_NF (SML #)
+  type_NF nat int (SML #)
 
 ML {*
 structure Norm = ROOT.WeakNorm;
 structure Type = ROOT.Type;
 structure Lambda = ROOT.Lambda;
+structure Nat = ROOT.Nat;
 
-fun nat_of_int 0 = ROOT.Nat.Zero_nat
-  | nat_of_int n = ROOT.Nat.Suc (nat_of_int (n-1));
-
-fun int_of_nat ROOT.Nat.Zero_nat = 0
-  | int_of_nat (ROOT.Nat.Suc n) = 1 + int_of_nat n;
+val nat_of_int = ROOT.Integer.nat;
+val int_of_nat = ROOT.Integer.int;
 
 fun dBtype_of_typ (Type ("fun", [T, U])) =
       Type.Fun (dBtype_of_typ T, dBtype_of_typ U)
@@ -622,7 +622,7 @@
       let val dBT = dBtype_of_typ T
       in Norm.Absa (e, dBT, dB_of_term t,
         dBtype_of_typ (fastype_of1 (T :: Ts, t)),
-        typing_of_term (T :: Ts) (Type.shift e ROOT.Nat.Zero_nat dBT) t)
+        typing_of_term (T :: Ts) (Type.shift e Nat.Zero_nat dBT) t)
       end
   | typing_of_term _ _ _ = error "typing_of_term: bad term";