--- a/ProgTutorial/Package/simple_inductive_package.ML	Sun Nov 22 03:13:29 2009 +0100
+++ b/ProgTutorial/Package/simple_inductive_package.ML	Sun Nov 22 15:27:10 2009 +0100
@@ -22,7 +22,7 @@
 fun make_defs ((binding, syn), trm) lthy =
 let 
   val arg = ((binding, syn), (Attrib.empty_binding, trm))
-  val ((_, (_ , thm)), lthy) = Local_Theory.define "" arg lthy
+  val ((_, (_ , thm)), lthy) = Local_Theory.define arg lthy
 in 
   (thm, lthy) 
 end