src/HOL/Integ/IntDef.thy

 attach (test) {*
 fun gen_int i = one_of [~1, 1] * random_range 0 i;
 *}
 
 definition
-  int_aux :: "int \<Rightarrow> nat \<Rightarrow> int"
+  int_aux :: "int \<Rightarrow> nat \<Rightarrow> int" where
   "int_aux i n = (i + int n)"
-  nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat"
+
+definition
+  nat_aux :: "nat \<Rightarrow> int \<Rightarrow> nat" where
   "nat_aux n i = (n + nat i)"
 
 lemma [code]:
   "int_aux i 0 = i"
   "int_aux i (Suc n) = int_aux (i + 1) n" -- {* tail recursive *}