--- a/ProgTutorial/Essential.thy	Sat Aug 31 08:07:45 2013 +0100
+++ b/ProgTutorial/Essential.thy	Sun Dec 15 23:49:05 2013 +0000
@@ -1769,7 +1769,7 @@
 
   @{ML_response_fake [display,gray,linenos]
   "Thm.reflexive @{cterm \"True\"}
-  |> Simplifier.rewrite_rule [@{thm True_def}]
+  |> Simplifier.rewrite_rule @{context} [@{thm True_def}]
   |> pretty_thm @{context}
   |> pwriteln"
   "(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"}
@@ -1785,7 +1785,7 @@
   replaces all object connectives by equivalents in the meta logic. For example
 
   @{ML_response_fake [display, gray]
-  "Object_Logic.rulify @{thm foo_test2}"
+  "Object_Logic.rulify @{context} @{thm foo_test2}"
   "\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C"}
 
   The transformation in the other direction can be achieved with function
@@ -1794,9 +1794,9 @@
   @{ML_response_fake [display,gray]
   "let
   val thm = @{thm foo_test1}
-  val meta_eq = Object_Logic.atomize (cprop_of thm)
+  val meta_eq = Object_Logic.atomize @{context} (cprop_of thm)
 in
-  Raw_Simplifier.rewrite_rule [meta_eq] thm
+  Raw_Simplifier.rewrite_rule @{context} [meta_eq] thm
 end"
   "?A \<longrightarrow> ?B \<longrightarrow> ?C"}
 
@@ -1815,19 +1815,19 @@
   following function for atomizing a theorem.
 *}
 
-ML %grayML{*fun atomize_thm thm =
+ML %grayML{*fun atomize_thm ctxt thm =
 let
   val thm' = forall_intr_vars thm
-  val thm'' = Object_Logic.atomize (cprop_of thm')
+  val thm'' = Object_Logic.atomize ctxt (cprop_of thm')
 in
-  Raw_Simplifier.rewrite_rule [thm''] thm'
+  Raw_Simplifier.rewrite_rule ctxt [thm''] thm'
 end*}
 
 text {*
   This function produces for the theorem @{thm [source] list.induct}
 
   @{ML_response_fake [display, gray]
-  "atomize_thm @{thm list.induct}"
+  "atomize_thm @{context} @{thm list.induct}"
   "\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}
 
   Theorems can also be produced from terms by giving an explicit proof.