diff -r 7675427e311f -r 36d61044f9bf ProgTutorial/Package/Ind_Code.thy
--- a/ProgTutorial/Package/Ind_Code.thy	Sun Nov 22 03:13:29 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Sun Nov 22 15:27:10 2009 +0100
@@ -28,43 +28,17 @@
 ML %linenosgray{*fun make_defn ((predname, mx), trm) lthy =
 let 
   val arg = ((predname, mx), (Attrib.empty_binding, trm))
-  val ((_, (_ , thm)), lthy') = Local_Theory.define "" 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, the string @{ML "\"\""} is a flag
-  attached to the theorem (other possibile flags are @{ML_ind  definitionK in Thm}
-  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
-  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
-*}
-
-local_setup %gray {* fn lthy =>
-let
-  val arg = ((@{binding "My_True"}, NoSyn), @{term True})
-  val (def, lthy') = make_defn arg lthy 
-in
-  tracing (string_of_thm_no_vars lthy' def); lthy'
-end *}
-
-text {*
-  which introduces the definition @{thm My_True_def} and then prints it out. 
-  Since we are testing the function inside \isacommand{local\_setup}, i.e., make
-  actual changes to the ambient theory, we can query the definition with the usual
-  command \isacommand{thm}:
-
-  \begin{isabelle}
-  \isacommand{thm}~@{thm [source] "My_True_def"}\\
-  @{text ">"}~@{thm "My_True_def"}
-  \end{isabelle}
-
+  definition has been made. We 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. 
+ 
   The next two functions construct the right-hand sides of the definitions, 
   which are terms whose general form is: