--- a/ProgTutorial/FirstSteps.thy	Wed Nov 18 14:06:01 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy	Thu Nov 19 14:11:50 2009 +0100
@@ -888,13 +888,12 @@
   "name"}
 
   An example where a qualified name is needed is the function 
-  @{ML_ind define in LocalTheory}.  This function is used below to define 
+  @{ML_ind define in Local_Theory}.  This function is used below to define 
   the constant @{term "TrueConj"} as the conjunction @{term "True \<and> True"}.
 *}
 
 local_setup %gray {* 
-  LocalTheory.define Thm.internalK 
-    ((@{binding "TrueConj"}, NoSyn), 
+  Local_Theory.define "" ((@{binding "TrueConj"}, NoSyn), 
       (Attrib.empty_binding, @{term "True \<and> True"})) #> snd *}
 
 text {*