# HG changeset patch
# User haftmann
# Date 1158672112 -7200
# Node ID 5af400cc64d5e57562fcc70ecbe5cfe63a5a2492
# Parent  527563e67194306f89463eb05b251b1ab0a76b7c
added some stuff for code generation 2

diff -r 527563e67194 -r 5af400cc64d5 src/HOL/Extraction/Higman.thy
--- a/src/HOL/Extraction/Higman.thy	Tue Sep 19 15:21:51 2006 +0200
+++ b/src/HOL/Extraction/Higman.thy	Tue Sep 19 15:21:52 2006 +0200
@@ -294,6 +294,9 @@
 contains
   test = good_prefix
 
+declare barT.recs(2) [where ?fun = ?func, code func]
+code_gen good_prefix (SML _) (SML "~~/src/codegen/generated/higman.ML")
+
 ML {*
 local open Higman in
 
diff -r 527563e67194 -r 5af400cc64d5 src/HOL/Extraction/Pigeonhole.thy
--- a/src/HOL/Extraction/Pigeonhole.thy	Tue Sep 19 15:21:51 2006 +0200
+++ b/src/HOL/Extraction/Pigeonhole.thy	Tue Sep 19 15:21:52 2006 +0200
@@ -285,6 +285,9 @@
 consts_code
   arbitrary :: "nat \<times> nat" ("{* (0::nat, 0::nat) *}")
 
+code_const "arbitrary \<Colon> nat \<times> nat"
+  (SML "{* (0\<Colon>nat, 0\<Colon>nat) *}")
+
 code_module PH
 contains
   test = "\<lambda>n. pigeonhole n (\<lambda>m. m - 1)"
diff -r 527563e67194 -r 5af400cc64d5 src/HOL/Extraction/QuotRem.thy
--- a/src/HOL/Extraction/QuotRem.thy	Tue Sep 19 15:21:51 2006 +0200
+++ b/src/HOL/Extraction/QuotRem.thy	Tue Sep 19 15:21:52 2006 +0200
@@ -49,4 +49,6 @@
 contains
   test = "division 9 2"
 
+code_gen division (SML -)
+
 end
diff -r 527563e67194 -r 5af400cc64d5 src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Tue Sep 19 15:21:51 2006 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Tue Sep 19 15:21:52 2006 +0200
@@ -448,6 +448,9 @@
 consts_code
   "some_elem" ("hd")
 
+code_const some_elem
+  (SML "{*hd*}")
+
 lemma JVM_sup_unfold [code]:
  "JVMType.sup S m n = lift2 (Opt.sup
        (Product.sup (Listn.sup (JType.sup S))