--- a/ProgTutorial/Package/Ind_Code.thy	Thu Feb 11 10:44:50 2010 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Sun Mar 07 21:15:05 2010 +0100
@@ -137,7 +137,7 @@
 ML %linenosgray{*fun defns rules preds prednames mxs arg_typss 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 (defn_aux lthy orules preds) (preds ~~ arg_typss) 
 in
   fold_map make_defn (prednames ~~ mxs ~~ defs) lthy
@@ -150,7 +150,7 @@
   meta-connectives). To do this transformation we have to obtain the theory
   behind the local theory using the function @{ML_ind  theory_of in ProofContext} 
   (Line 3); with this theory we can use the function
-  @{ML_ind  atomize_term in ObjectLogic} to make the transformation (Line 4). The call
+  @{ML_ind  atomize_term in Object_Logic} to make the transformation (Line 4). The call
   to @{ML defn_aux} in Line 5 produces all right-hand sides of the
   definitions. The actual definitions are then made in Line 7.  The result of
   the function is a list of theorems and a local theory (the theorems are
@@ -254,7 +254,7 @@
 *}
 
 ML %linenosgray{*fun ind_tac defs prem insts =
-  EVERY1 [ObjectLogic.full_atomize_tac,
+  EVERY1 [Object_Logic.full_atomize_tac,
           cut_facts_tac prem,
           rewrite_goal_tac defs,
           inst_spec_tac insts,
@@ -540,7 +540,7 @@
 *}
 
 ML %linenosgray{*fun expand_tac defs =
-  ObjectLogic.rulify_tac 1
+  Object_Logic.rulify_tac 1
   THEN rewrite_goal_tac defs 1
   THEN (REPEAT (resolve_tac [@{thm allI}, @{thm impI}] 1)) *}
 
@@ -679,7 +679,7 @@
 
   To use this premise with @{ML rtac}, we need to instantiate its 
   quantifiers (with @{text params1}) and transform it into rule 
-  format (using @{ML_ind  rulify in ObjectLogic}). So we can modify the 
+  format (using @{ML_ind  rulify in Object_Logic}). So we can modify the 
   code as follows:
 *}
 
@@ -690,7 +690,7 @@
     val (params1, params2) = chop (length cparams - length preds) cparams
     val (prems1, prems2) = chop (length prems - length rules) prems
   in
-    rtac (ObjectLogic.rulify (all_elims params1 (nth prems2 i))) 1
+    rtac (Object_Logic.rulify (all_elims params1 (nth prems2 i))) 1
   end) *}
 
 text {* 
@@ -763,7 +763,7 @@
     val (params1, params2) = chop (length cparams - length preds) cparams
     val (prems1, prems2) = chop (length prems - length rules) prems
   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 (prepare_prem params2 prems2) prems1)
   end) *}
 
@@ -861,7 +861,7 @@
     val (params1, params2) = chop (length cparams - length preds) cparams
     val (prems1, prems2) = chop (length prems - length rules) prems
   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 (prepare_prem params2 prems2 context) prems1)
   end) *}
 
@@ -882,7 +882,7 @@
 *}
 
 ML %linenosgray{*fun intro_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}]),
           prove_intro_tac i preds rules ctxt]*}