diff -r fb6c29a90003 -r d8c376662bb4 ProgTutorial/Package/Ind_Extensions.thy
--- a/ProgTutorial/Package/Ind_Extensions.thy	Mon Apr 30 12:36:32 2012 +0100
+++ b/ProgTutorial/Package/Ind_Extensions.thy	Mon Apr 30 14:43:52 2012 +0100
@@ -192,10 +192,10 @@
 
 text {* Type declarations *}
 
-ML{*Typedef.add_typedef_global false NONE (@{binding test},[],NoSyn)
+ML %grayML{*Typedef.add_typedef_global false NONE (@{binding test},[],NoSyn)
   @{term "{1}::nat set"} NONE (simp_tac @{simpset} 1) @{theory} *}
 
-ML{*fun pat_completeness_auto ctxt =
+ML %grayML{*fun pat_completeness_auto ctxt =
   Pat_Completeness.pat_completeness_tac ctxt 1
     THEN auto_tac ctxt*}
 
@@ -213,4 +213,4 @@
     [(Attrib.empty_binding, @{term "\<And>x. baz (Foo x) = x"})]
       conf pat_completeness_auto #> snd*}
 
-(*<*)end(*>*)
\ No newline at end of file
+(*<*)end(*>*)