--- a/ProgTutorial/Package/simple_inductive_package.ML	Wed Nov 18 14:06:01 2009 +0100
+++ b/ProgTutorial/Package/simple_inductive_package.ML	Thu Nov 19 14:11:50 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) = LocalTheory.define Thm.internalK arg lthy
+  val ((_, (_ , thm)), lthy) = Local_Theory.define "" arg lthy
 in 
   (thm, lthy) 
 end
@@ -180,12 +180,12 @@
   val case_names = map (Binding.name_of o fst o fst) specs
 in
     lthy1 
-    |> LocalTheory.notes Thm.theoremK (map (fn (((a, atts), _), th) =>
+    |> Local_Theory.notes (map (fn (((a, atts), _), th) =>
         ((Binding.qualify false mut_name a, atts), [([th], [])])) (specs ~~ intros)) 
-    |-> (fn intross => LocalTheory.note Thm.theoremK
+    |-> (fn intross => Local_Theory.note 
          ((Binding.qualify false mut_name (Binding.name "intros"), []), maps snd intross)) 
     |>> snd 
-    ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>
+    ||>> (Local_Theory.notes (map (fn (((R, _), _), th) =>
          ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"),
           [Attrib.internal (K (Rule_Cases.case_names case_names)),
            Attrib.internal (K (Rule_Cases.consumes 1)),