Auxiliary functions to be used in generated code are now defined using "attach".

--- a/src/HOL/Integ/IntDef.thy	Tue Jul 12 11:41:24 2005 +0200
+++ b/src/HOL/Integ/IntDef.thy	Tue Jul 12 11:51:31 2005 +0200
@@ -855,17 +855,16 @@
 
 subsection {* Configuration of the code generator *}
 
-ML {*
-infix 7 `*;
-infix 6 `+;
-
-val op `* = op * : int * int -> int;
-val op `+ = op + : int * int -> int;
-val `~ = ~ : int -> int;
-*}
+(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
 
 types_code
   "int" ("int")
+attach (term_of) {*
+val term_of_int = HOLogic.mk_int o IntInf.fromInt;
+*}
+attach (test) {*
+fun gen_int i = one_of [~1, 1] * random_range 0 i;
+*}
 
 constdefs
   int_aux :: "int \<Rightarrow> nat \<Rightarrow> int"
@@ -889,9 +888,9 @@
 consts_code
   "0" :: "int"                  ("0")
   "1" :: "int"                  ("1")
-  "uminus" :: "int => int"      ("`~")
-  "op +" :: "int => int => int" ("(_ `+/ _)")
-  "op *" :: "int => int => int" ("(_ `*/ _)")
+  "uminus" :: "int => int"      ("~")
+  "op +" :: "int => int => int" ("(_ +/ _)")
+  "op *" :: "int => int => int" ("(_ */ _)")
   "op <" :: "int => int => bool" ("(_ </ _)")
   "op <=" :: "int => int => bool" ("(_ <=/ _)")
   "neg"                         ("(_ < 0)")

--- a/src/HOL/Library/EfficientNat.thy	Tue Jul 12 11:41:24 2005 +0200
+++ b/src/HOL/Library/EfficientNat.thy	Tue Jul 12 11:51:31 2005 +0200
@@ -30,16 +30,26 @@
 returns @{text "0"}.
 *}
 
-types_code nat ("int")
+types_code
+  nat ("int")
+attach (term_of) {*
+fun term_of_nat 0 = Const ("0", HOLogic.natT)
+  | term_of_nat 1 = Const ("1", HOLogic.natT)
+  | term_of_nat i = HOLogic.number_of_const HOLogic.natT $
+      HOLogic.mk_bin (IntInf.fromInt i);
+*}
+attach (test) {*
+fun gen_nat i = random_range 0 i;
+*}
+
 consts_code
   0 :: nat ("0")
   Suc ("(_ + 1)")
-  nat ("nat")
-  int ("(_)")
-
-ML {*
+  nat ("\<module>nat")
+attach {*
 fun nat i = if i < 0 then 0 else i;
 *}
+  int ("(_)")
 
 text {*
 Case analysis on natural numbers is rephrased using a conditional

--- a/src/HOL/List.thy	Tue Jul 12 11:41:24 2005 +0200
+++ b/src/HOL/List.thy	Tue Jul 12 11:51:31 2005 +0200
@@ -2282,27 +2282,31 @@
    Codegen.add_codegen "char_codegen" char_codegen];
 
 end;
-
+*}
+
+types_code
+  "list" ("_ list")
+attach (term_of) {*
 val term_of_list = HOLogic.mk_list;
-
+*}
+attach (test) {*
 fun gen_list' aG i j = frequency
   [(i, fn () => aG j :: gen_list' aG (i-1) j), (1, fn () => [])] ()
 and gen_list aG i = gen_list' aG i i;
-
+*}
+  "char" ("string")
+attach (term_of) {*
 val nibbleT = Type ("List.nibble", []);
 
 fun term_of_char c =
   Const ("List.char.Char", nibbleT --> nibbleT --> Type ("List.char", [])) $
     Const ("List.nibble.Nibble" ^ nibble_of_int (ord c div 16), nibbleT) $
     Const ("List.nibble.Nibble" ^ nibble_of_int (ord c mod 16), nibbleT);
-
+*}
+attach (test) {*
 fun gen_char i = chr (random_range (ord "a") (Int.min (ord "a" + i, ord "z")));
 *}
 
-types_code
-  "list" ("_ list")
-  "char" ("string")
-
 consts_code "Cons" ("(_ ::/ _)")
 
 setup list_codegen_setup

--- a/src/HOL/Main.thy	Tue Jul 12 11:41:24 2005 +0200
+++ b/src/HOL/Main.thy	Tue Jul 12 11:51:31 2005 +0200
@@ -19,6 +19,12 @@
 
 types_code
   "bool"  ("bool")
+attach (term_of) {*
+fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
+*}
+attach (test) {*
+fun gen_bool i = one_of [false, true];
+*}
 
 consts_code
   "True"    ("true")
@@ -28,18 +34,14 @@
   "op &"    ("(_ andalso/ _)")
   "HOL.If"      ("(if _/ then _/ else _)")
 
-  "wfrec"   ("wf'_rec?")
+  "wfrec"   ("\<module>wf'_rec?")
+attach {*
+fun wf_rec f x = f (wf_rec f) x;
+*}
 
 quickcheck_params [default_type = int]
 
-(*FIXME: the IntInf.fromInt below hides a dependence on fixed-precision ints!*)
 ML {*
-fun wf_rec f x = f (wf_rec f) x;
-
-fun term_of_bool b = if b then HOLogic.true_const else HOLogic.false_const;
-val term_of_int = HOLogic.mk_int o IntInf.fromInt;
-fun term_of_fun_type _ T _ U _ = Free ("<function>", T --> U);
-
 local
 
 fun eq_codegen thy defs gr dep thyname b t =
@@ -62,20 +64,6 @@
 val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];
 
 end;
-
-fun gen_bool i = one_of [false, true];
-
-fun gen_int i = one_of [~1, 1] * random_range 0 i;
-
-fun gen_fun_type _ G i =
-  let
-    val f = ref (fn x => raise ERROR);
-    val _ = (f := (fn x =>
-      let
-        val y = G i;
-        val f' = !f
-      in (f := (fn x' => if x = x' then y else f' x'); y) end))
-  in (fn x => !f x) end;
 *}
 
 setup eq_codegen_setup

--- a/src/HOL/MicroJava/J/JListExample.thy	Tue Jul 12 11:41:24 2005 +0200
+++ b/src/HOL/MicroJava/J/JListExample.thy	Tue Jul 12 11:51:31 2005 +0200
@@ -65,7 +65,12 @@
   loc_ ("int")
 
 consts_code
-  "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *} {* Loc *}")
+  "new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *} {* Loc *}")
+attach {*
+fun new_addr p none loc hp =
+  let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
+  in nr 0 end;
+*}
 
   "arbitrary" ("(raise ERROR)")
   "arbitrary" :: "val" ("{* Unit *}")
@@ -82,12 +87,6 @@
   "l3_nam" ("\"l3\"")
   "l4_nam" ("\"l4\"")
 
-ML {*
-fun new_addr p none loc hp =
-  let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
-  in nr 0 end;
-*}
-
 generate_code
   test = "example_prg\<turnstile>Norm (empty, empty)
     -(Expr (l1_name::=NewC list_name);;

--- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Jul 12 11:41:24 2005 +0200
+++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Jul 12 11:51:31 2005 +0200
@@ -94,7 +94,12 @@
   loc_ ("int")
 
 consts_code
-  "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
+  "new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}")
+attach {*
+fun new_addr p none loc hp =
+  let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
+  in nr 0 end;
+*}
 
   "arbitrary" ("(raise ERROR)")
   "arbitrary" :: "val" ("{* Unit *}")
@@ -107,12 +112,6 @@
   "val_nam" ("\"val\"")
   "next_nam" ("\"next\"")
 
-ML {*
-fun new_addr p none loc hp =
-  let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1);
-  in nr 0 end;
-*}
-
 subsection {* Single step execution *}
 
 generate_code

--- a/src/HOL/Product_Type.thy	Tue Jul 12 11:41:24 2005 +0200
+++ b/src/HOL/Product_Type.thy	Tue Jul 12 11:51:31 2005 +0200
@@ -773,6 +773,12 @@
 
 types_code
   "*"     ("(_ */ _)")
+attach (term_of) {*
+fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
+*}
+attach (test) {*
+fun gen_id_42 aG bG i = (aG i, bG i);
+*}
 
 consts_code
   "Pair"    ("(_,/ _)")
@@ -780,10 +786,6 @@
   "snd"     ("snd")
 
 ML {*
-fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
-
-fun gen_id_42 aG bG i = (aG i, bG i);
-
 local
 
 fun strip_abs 0 t = ([], t)