--- a/ProgTutorial/Package/Ind_Code.thy	Thu Nov 05 10:30:59 2009 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Sat Nov 07 01:03:37 2009 +0100
@@ -1005,8 +1005,8 @@
         ||>> note_many mut_name ((@{binding "inducts"}, []), ind_prins)
         ||>> fold_map (note_single1 mut_name) (namesattrs ~~ intro_rules)  
         ||>> fold_map (note_single2 @{binding "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 ""))]) 
              (prednames ~~ ind_prins) 
         |> snd
@@ -1043,9 +1043,9 @@
   Line 20 add further every introduction rule under its own name
   (given by the user).\footnote{FIXME: what happens if the user did not give
   any name.} Line 21 registers the induction principles. For this we have
-  to use some specific attributes. The first @{ML_ind  case_names in RuleCases} 
+  to use some specific attributes. The first @{ML_ind  case_names in Rule_Cases} 
   corresponds to the case names that are used by Isar to reference the proof
-  obligations in the induction. The second @{ML "consumes 1" in RuleCases}
+  obligations in the induction. The second @{ML "consumes 1" in Rule_Cases}
   indicates that the first premise of the induction principle (namely
   the predicate over which the induction proceeds) is eliminated.