diff -r 96d10631eec2 -r 4b96e3c8b33e ProgTutorial/Recipes/CallML.thy
--- a/ProgTutorial/Recipes/CallML.thy	Mon Dec 31 20:20:55 2012 +0000
+++ b/ProgTutorial/Recipes/CallML.thy	Mon Feb 25 00:33:48 2013 +0000
@@ -1,7 +1,7 @@
 (*<*)
 theory CallML
 imports "~~/src/HOL/Number_Theory/Primes" 
-        "~~/src/HOL/Library/Efficient_Nat"
+        "~~/src/HOL/Library/Code_Target_Numeral"
 begin
 (*>*)
 
@@ -53,12 +53,12 @@
   from ML, e.g.\ a computer algebra system.
 
   It should be noted, however, that in this example you need to import the
-  theory @{theory Efficient_Nat} in order to force the HOL-type @{typ nat} to
+  theory @{theory Code_Target_Numeral} in order to force the HOL-type @{typ nat} to
   be implemented by the ML-type @{text "int"}. 
 
   \begin{graybox}\small
   \isacommand{theory}~@{text CallML}\\
-  \isacommand{imports}~@{text Main} @{text [quotes] "~~/src/HOL/Library/Efficient_Nat"}\\
+  \isacommand{imports}~@{text Main} @{text [quotes] "~~/src/HOL/Library/Code_Target_Numeral"}\\
   ...
   \end{graybox}
 
@@ -68,7 +68,16 @@
   to connect the two levels:
 *}
 
-code_const factor (SML "factor")
+definition factor_integer :: "integer \<Rightarrow> integer"
+where
+  [code del]: "factor_integer = integer_of_nat \<circ> factor \<circ> nat_of_integer"
+
+lemma [code]:
+  "factor = nat_of_integer \<circ> factor_integer \<circ> integer_of_nat"
+  by (simp add: factor_integer_def fun_eq_iff)
+
+code_const factor_integer (SML "factor")
+code_reserved SML factor
 
 text{* 
   The result of this declaration is that the HOL-function @{const factor} 
@@ -100,7 +109,7 @@
 
   The above example was easy because we forced Isabelle (via the inclusion of the
   theory @{theory
-  Efficient_Nat}) to implement @{typ nat} by @{text int}, a predefined 
+  Code_Target_Numeral}) to implement @{typ nat} by @{text int}, a predefined 
   ML-type.  By default, Isabelle implements, for example, the HOL-type 
   @{text list} by the corresponding ML-type. Thus the following variation 
   on @{const factor} also works: 
@@ -108,9 +117,17 @@
 
 consts factor2 :: "nat \<Rightarrow> nat list" (*<*)(*>*)
 ML %grayML{*fun factor2 n = if n = 4 then [2] else []*}(*<*)(*>*)
-code_const factor2 (SML "factor2")
+
+definition factor2_integer :: "integer \<Rightarrow> integer list"
+where
+  [code del]: "factor2_integer = map integer_of_nat \<circ> factor2 \<circ> nat_of_integer"
 
-value "factor2 4"
+lemma [code]:
+  "factor2 = map nat_of_integer \<circ> factor2_integer \<circ> integer_of_nat"
+  by (simp add: factor2_integer_def fun_eq_iff comp_def)
+
+code_const factor2_integer (SML "factor2")
+code_reserved SML factor2
 
 text{* 
   The first line declares the type of @{const factor2}; the second
@@ -120,51 +137,9 @@
   @{text bool}, @{text int}, @{text list}, @{text option} and pairs, 
   only. If you have arbitrary tuples, for example, then you have to code 
   them as nested pairs.
-
-  Let us now look at how to refer to user-defined HOL-datatypes from the
-  ML-level. We modify our @{const factor} example a little by introducing a new
-  datatype for the result: 
-*}
-
-datatype result = Factor nat | Prime
-
-consts factor' :: "nat \<Rightarrow> result"
-
-text{* 
-  In order to write ML-code that uses this datatype, we need to define
-  this datatype at the ML-level first. The following command does just that. 
 *}
 
-code_reflect Result
-  datatypes result = Factor | Prime
-
-text{* 
-  This creates an ML-structure called @{text Result} (the name can be
-  arbitrarily chosen) that contains the datatype @{typ result}. The list 
-  of constructors (but not their types) needs to be given. Now we can 
-  write ML-code that uses this datatype: 
-*}
-
-ML %grayML{*fun factor' n = if n = 4 then Result.Factor 2 else Result.Prime*}
-
-text{* 
-  Finally we can link the HOL and ML version of @{const factor'} as
-  before: 
-*}
-
-code_const factor' (SML "factor'")
-
-text{* 
-  Now any evaluation of the HOL function @{const factor'} will use the
-  corresponding ML-function, like in the examples for @{const factor} above.
-
-  In general, \isacommand{code\_reflect} can export multiple datatypes 
-  (separated by \isacommand{and}) and also HOL-functions: simply add a line
-  \isacommand{functions} $f_1$ $f_2$ and so on.
-*}
-
-(*<*)
-value "factor' 4"
+value "factor2 4"
 
 end
 (*>*)