--- a/ProgTutorial/Essential.thy	Tue Jun 08 15:18:30 2010 +0200
+++ b/ProgTutorial/Essential.thy	Mon Jul 19 15:44:13 2010 +0100
@@ -244,7 +244,7 @@
 
    @{ML_response [display,gray]
   "@{typ \"bool \<Rightarrow> nat\"}"
-  "Type (\"fun\", [Type (\"bool\", []), Type (\"nat\", [])])"}
+  "Type (\"fun\", [Type (\"bool\", []), Type (\"Nat.nat\", [])])"}
 
   We can restore the usual behaviour of Isabelle's pretty printer
   with the code
@@ -303,7 +303,7 @@
 
   @{ML_response [display,gray] "make_imp @{term S} @{term T}" 
 "Const \<dots> $ 
-  Abs (\"x\", Type (\"nat\",[]),
+  Abs (\"x\", Type (\"Nat.nat\",[]),
     Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"}
 
   whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"} 
@@ -341,7 +341,7 @@
 in
   lambda x_nat trm
 end"
-  "Abs (\"x\", \"nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
+  "Abs (\"x\", \"Nat.nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
 
   In this example, @{ML lambda} produces a de Bruijn index (i.e.~@{ML "Bound 0"}), 
   and an abstraction, where it also records the type of the abstracted
@@ -446,7 +446,7 @@
 in
   Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, body)
 end"
-  "(\"xa\", Free (\"xa\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}
+  "(\"xa\", Free (\"xa\", \"Nat.nat \<Rightarrow> bool\") $ Free (\"x\", \"Nat.nat\"))"}
 
   There are also many convenient functions that construct specific HOL-terms
   in the structure @{ML_struct HOLogic}. For example @{ML_ind mk_eq in

Binary file progtutorial.pdf has changed