--- a/ProgTutorial/Package/Ind_Code.thy	Mon Oct 17 13:30:49 2011 +0100
+++ b/ProgTutorial/Package/Ind_Code.thy	Wed Oct 26 12:59:44 2011 +0100
@@ -136,7 +136,7 @@
 
 ML %linenosgray{*fun defns rules preds prednames mxs arg_typss lthy =
 let
-  val thy = ProofContext.theory_of lthy
+  val thy = Proof_Context.theory_of lthy
   val orules = map (Object_Logic.atomize_term thy) rules
   val defs = map (defn_aux lthy orules preds) (preds ~~ arg_typss) 
 in
@@ -148,7 +148,7 @@
   meta-quanti\-fications. In Line 4, we transform these introduction rules
   into the object logic (since definitions cannot be stated with
   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} 
+  behind the local theory using the function @{ML_ind theory_of in Proof_Context} 
   (Line 3); with this theory we can use the function
   @{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
@@ -341,7 +341,7 @@
 in
   Goal.prove lthy' [] [prem] goal
       (fn {prems, ...} => ind_tac defs prems cnewpreds)
-  |> singleton (ProofContext.export lthy' lthy)
+  |> singleton (Proof_Context.export lthy' lthy)
 end *}
 
 text {* 
@@ -405,7 +405,7 @@
   val Ps = replicate (length preds) "P"
   val (newprednames, lthy') = Variable.variant_fixes Ps lthy
   
-  val thy = ProofContext.theory_of lthy'
+  val thy = Proof_Context.theory_of lthy'
 
   val tyss' = map (fn tys => tys ---> HOLogic.boolT) arg_tyss
   val newpreds = map Free (newprednames ~~ tyss')
@@ -415,7 +415,7 @@
 in
   map (prove_ind lthy' defs srules cnewpreds) 
         (preds ~~ newpreds ~~ arg_tyss)
-          |> ProofContext.export lthy' lthy
+          |> Proof_Context.export lthy' lthy
 end*}
 
 text {*