--- a/ProgTutorial/Base.thy	Mon Oct 17 13:30:49 2011 +0100
+++ b/ProgTutorial/Base.thy	Wed Oct 26 12:59:44 2011 +0100
@@ -54,7 +54,7 @@
 let
   val pre  = implode ["\n", "local_setup ", "{", "*", "\n"]
   val post = implode ["\n", "*", "}", "\n"]
-  val _ = write_file (enclose pre post txt) (ProofContext.theory_of lthy)
+  val _ = write_file (enclose pre post txt) (Proof_Context.theory_of lthy)
 in
   lthy
 end