--- a/ProgTutorial/Essential.thy	Sat Aug 28 13:37:25 2010 +0800
+++ b/ProgTutorial/Essential.thy	Fri Oct 29 11:00:37 2010 +0100
@@ -38,7 +38,7 @@
 
   @{ML_response [display,gray] 
 "@{term \"(a::nat) + b = c\"}" 
-"Const (\"op =\", \<dots>) $ 
+"Const (\"HOL.eq\", \<dots>) $ 
   (Const (\"Groups.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
 
   constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using 
@@ -1092,10 +1092,10 @@
   also tries first to solve the problem by higher-order pattern
   unification. Only in case of failure full higher-order unification is
   called. This function has a built-in bound, which can be accessed and
-  manipulated as a configuration value:
+  manipulated as a configuration value. For example
 
   @{ML_response_fake [display,gray]
-  "Config.get_global @{theory} (Unify.search_bound_value)"
+  "Config.get_global @{theory} (Unify.search_bound)"
   "Int 60"}
 
   If this bound is reached during unification, Isabelle prints out the
@@ -1538,7 +1538,7 @@
   also a bit too restrictive in cases where a theorem name should refer to a 
   dynamically expanding list of theorems (like a simpset). Therefore Isabelle 
   also implements a mechanism where a theorem name can refer to a custom theorem 
-  list. For this you can use the function @{ML_ind add_thms_dynamic in PureThy}. 
+  list. For this you can use the function @{ML_ind add_thms_dynamic in Global_Theory}. 
   To see how it works let us assume we defined our own theorem list @{text MyThmList}.
 *}
 
@@ -1560,11 +1560,11 @@
 text {*
   We can now install the theorem list so that it is visible to the user and 
   can be refered to by a theorem name. For this need to call 
-  @{ML_ind add_thms_dynamic in PureThy}
+  @{ML_ind add_thms_dynamic in Global_Theory}
 *}
 
 setup %gray {* 
-  PureThy.add_thms_dynamic (@{binding "mythmlist"}, MyThmList.get) 
+  Global_Theory.add_thms_dynamic (@{binding "mythmlist"}, MyThmList.get) 
 *}
 
 text {*