--- a/ProgTutorial/Recipes/CallML.thy	Wed Jun 20 08:53:38 2012 +0100
+++ b/ProgTutorial/Recipes/CallML.thy	Wed Jun 20 09:42:18 2012 +0100
@@ -54,7 +54,16 @@
 
   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
-  be implemented by the ML-type @{text "int"}. Thus the ML implementation of
+  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"}\\
+  ...
+  \end{graybox}
+
+
+  Thus the ML implementation of
   @{const factor} must be and is of type @{text "int -> int"}. Now it is time
   to connect the two levels:
 *}

Binary file progtutorial.pdf has changed