--- a/ProgTutorial/First_Steps.thy	Fri May 17 11:01:55 2013 +0100
+++ b/ProgTutorial/First_Steps.thy	Tue May 28 23:26:18 2013 +0100
@@ -166,22 +166,7 @@
   "(1::nat, x::'a)"}
 
   where @{text 1} and @{text x} are displayed with their inferred type.
-  Even more type information can be printed by setting 
-  the reference @{ML_ind show_all_types in Syntax} to @{ML true}. 
-  In this case we obtain
-*}
-
-text {*
-  @{ML_response_fake [display, gray]
-  "let 
-  val show_all_types_ctxt = Config.put show_all_types true @{context}
-in
-  pwriteln (pretty_term show_all_types_ctxt @{term \"(1::nat, x)\"})
-end"
-  "(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}
-
-  where now even @{term Pair} is written with its type (@{term Pair} is the
-  term-constructor for products). Other configuration values that influence
+  Other configuration values that influence
   printing of terms include 
 
   \begin{itemize}

--- a/ProgTutorial/Package/Ind_Extensions.thy	Fri May 17 11:01:55 2013 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Tue May 28 23:26:18 2013 +0100
@@ -192,8 +192,10 @@
 
 text {* Type declarations *}
 
+(*
 ML %grayML{*Typedef.add_typedef_global (@{binding test}, [], NoSyn)
   @{term "{1}::nat set"} NONE (simp_tac @{context} 1) @{theory} *}
+*)
 
 ML %grayML{*fun pat_completeness_auto ctxt =
   Pat_Completeness.pat_completeness_tac ctxt 1

--- a/ProgTutorial/Parsing.thy	Fri May 17 11:01:55 2013 +0100
+++ b/ProgTutorial/Parsing.thy	Tue May 28 23:26:18 2013 +0100
@@ -1513,7 +1513,7 @@
 oops
 
 method_setup joker = {* 
-  Scan.lift (Scan.succeed (fn ctxt => Method.cheating true)) *} {* bla *}
+  Scan.lift (Scan.succeed (fn ctxt => Method.cheating ctxt true)) *} {* bla *}
 
 lemma "False"
 apply(joker)

Binary file progtutorial.pdf has changed