src/HOL/ex/Fundefs.thy

   (if n \<le> 1 then Some [n]
    else if even n 
      then do { ns \<leftarrow> collatz (n div 2); Some (n # ns) }
      else do { ns \<leftarrow> collatz (3 * n + 1);  Some (n # ns)})"
 
-declare collatz.rec[code]
+declare collatz.simps[code]
 value "collatz 23"
 
 
 text {* Tail-recursive functions: *}