diff -r fea1b7ce5c4a -r 25371f74c768 ProgTutorial/Package/simple_inductive_package.ML
--- a/ProgTutorial/Package/simple_inductive_package.ML	Mon Oct 17 13:30:49 2011 +0100
+++ b/ProgTutorial/Package/simple_inductive_package.ML	Wed Oct 26 12:59:44 2011 +0100
@@ -49,7 +49,7 @@
 (* @chunk definitions *) 
 fun definitions rules params preds prednames syns arg_typess 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 (defs_aux lthy orules preds params) (preds ~~ arg_typess) 
@@ -78,7 +78,7 @@
   val Ps = replicate (length preds) "P"
   val (newprednames, lthy3) = Variable.variant_fixes Ps lthy2
 
-  val thy = ProofContext.theory_of lthy3			      
+  val thy = Proof_Context.theory_of lthy3			      
 
   val Tss' = map (fn Ts => Ts ---> HOLogic.boolT) Tss
   val newpreds = map Free (newprednames ~~ Tss')
@@ -97,7 +97,7 @@
   in
     Goal.prove lthy4 [] [prem] goal
       (fn {prems, ...} => induction_tac defs prems cnewpreds)
-      |> singleton (ProofContext.export lthy4 lthy1)
+      |> singleton (Proof_Context.export lthy4 lthy1)
   end 
 in
   map prove_induction (preds ~~ newpreds ~~ Tss)
@@ -152,7 +152,7 @@
   fun prove_intro (i, goal) =
     Goal.prove lthy2 [] [] goal
        (fn {context, ...} => introductions_tac defs rules preds i context)
-       |> singleton (ProofContext.export lthy2 lthy1)
+       |> singleton (Proof_Context.export lthy2 lthy1)
 in
   map_index prove_intro rules
 end