--- a/ProgTutorial/Package/simple_inductive_package.ML	Thu Nov 05 10:30:59 2009 +0100
+++ b/ProgTutorial/Package/simple_inductive_package.ML	Sat Nov 07 01:03:37 2009 +0100
@@ -187,8 +187,8 @@
     |>> snd 
     ||>> (LocalTheory.notes Thm.theoremK (map (fn (((R, _), _), th) =>
          ((Binding.qualify false (Binding.name_of R) (Binding.name "induct"),
-          [Attrib.internal (K (RuleCases.case_names case_names)),
-           Attrib.internal (K (RuleCases.consumes 1)),
+          [Attrib.internal (K (Rule_Cases.case_names case_names)),
+           Attrib.internal (K (Rule_Cases.consumes 1)),
            Attrib.internal (K (Induct.induct_pred ""))]), [([th], [])]))
           (preds ~~ inducts)) #>> maps snd) 
     |> snd