--- a/ProgTutorial/Package/simple_inductive_package.ML	Thu Feb 11 10:44:50 2010 +0100
+++ b/ProgTutorial/Package/simple_inductive_package.ML	Sun Mar 07 21:15:05 2010 +0100
@@ -50,7 +50,7 @@
 fun definitions rules params preds prednames syns arg_typess lthy =
 let
   val thy = ProofContext.theory_of lthy
-  val orules = map (ObjectLogic.atomize_term thy) rules
+  val orules = map (Object_Logic.atomize_term thy) rules
   val defs = 
     map (defs_aux lthy orules preds params) (preds ~~ arg_typess) 
 in
@@ -63,7 +63,7 @@
 
 (* @chunk induction_tac *)
 fun induction_tac defs prems insts =
-  EVERY1 [ObjectLogic.full_atomize_tac,
+  EVERY1 [Object_Logic.full_atomize_tac,
           cut_facts_tac prems,
           rewrite_goal_tac defs,
           EVERY' (map (dtac o inst_spec) insts),
@@ -131,14 +131,14 @@
     val (prems1, prems2) = chop (length prems - length rules) prems;
     val (params1, params2) = chop (length params - length preds) (map snd params);
   in
-    rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1 
+    rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1 
     THEN
     EVERY1 (map (fn prem => subproof2 prem params2 prems2 ctxt') prems1)
   end)
 (* @end *)
 
 fun introductions_tac defs rules preds i ctxt =
-  EVERY1 [ObjectLogic.rulify_tac,
+  EVERY1 [Object_Logic.rulify_tac,
           rewrite_goal_tac defs,
           REPEAT o (resolve_tac [@{thm allI},@{thm impI}]),
           subproof1 rules preds i ctxt]