--- a/ProgTutorial/Package/Ind_Code.thy	Wed Nov 18 14:06:01 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Thu Nov 19 14:11:50 2009 +0100
@@ -21,27 +21,27 @@
 
   and then ``register'' the definition inside a local theory. 
   To do the latter, we use the following wrapper for the function
-  @{ML_ind  define in LocalTheory}. The wrapper takes a predicate name, a syntax
+  @{ML_ind define in Local_Theory}. The wrapper takes a predicate name, a syntax
   annotation and a term representing the right-hand side of the definition.
 *}
 
 ML %linenosgray{*fun make_defn ((predname, mx), trm) lthy =
 let 
   val arg = ((predname, mx), (Attrib.empty_binding, trm))
-  val ((_, (_ , thm)), lthy') = LocalTheory.define Thm.internalK arg lthy
+  val ((_, (_ , thm)), lthy') = Local_Theory.define "" arg lthy
 in 
   (thm, lthy') 
 end*}
 
 text {*
   It returns the definition (as a theorem) and the local theory in which the
-  definition has been made. In Line 4, @{ML_ind  internalK in Thm} is a flag
+  definition has been made. In Line 4, the string @{ML "\"\""} is a flag
   attached to the theorem (other possibile flags are @{ML_ind  definitionK in Thm}
-  and @{ML_ind  axiomK in Thm}).\footnote{\bf FIXME: move to theorem section.} 
+  and @{ML_ind theoremK in Thm}).\footnote{\bf FIXME: move to theorem section.} 
   These flags just classify theorems and have no
   significant meaning, except for tools that, for example, find theorems in
   the theorem database.\footnote{FIXME: put in the section about theorems.} We
-  also use @{ML_ind  empty_binding in Attrib} in Line 3, since the definitions for
+  also use @{ML_ind empty_binding in Attrib} in Line 3, since the definitions for
   our inductive predicates are not meant to be seen by the user and therefore
   do not need to have any theorem attributes. A testcase for this function is
 *}
@@ -961,7 +961,7 @@
   We have produced various theorems (definitions, induction principles and
   introduction rules), but apart from the definitions, we have not yet 
   registered them with the theorem database. This is what the functions 
-  @{ML_ind  note in LocalTheory} does. 
+  @{ML_ind  note in Local_Theory} does. 
 
 
   For convenience, we use the following 
@@ -969,8 +969,7 @@
 *}
 
 ML{*fun note_many qname ((name, attrs), thms) = 
-  LocalTheory.note Thm.theoremK 
-    ((Binding.qualify false qname name, attrs), thms) 
+  Local_Theory.note ((Binding.qualify false qname name, attrs), thms) 
 
 fun note_single1 qname ((name, attrs), thm) = 
   note_many qname ((name, attrs), [thm])