--- a/ProgTutorial/Essential.thy	Sun Oct 30 17:45:10 2011 +0000
+++ b/ProgTutorial/Essential.thy	Wed Nov 02 13:38:19 2011 +0000
@@ -263,8 +263,7 @@
   we can see the full name of the type is actually @{text "List.list"}, indicating
   that it is defined in the theory @{text "List"}. However, one has to be 
   careful with names of types, because even if
-  @{text "fun"}, @{text "bool"} and @{text "nat"} are defined in the 
-  theories @{text "HOL"} and @{text "Nat"}, respectively, they are 
+  @{text "fun"} is defined in the theory @{text "HOL"}, it is  
   still represented by their simple name.
 
    @{ML_response [display,gray]
@@ -384,7 +383,7 @@
 end"
   "Abs (\"x\", \"int\", Free (\"P\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}
 
-  then the variable @{text "Free (\"x\", \"int\")"} is \emph{not} abstracted. 
+  then the variable @{text "Free (\"x\", \"nat\")"} is \emph{not} abstracted. 
   This is a fundamental principle
   of Church-style typing, where variables with the same name still differ, if they 
   have different type.