diff -r 105715a0a807 -r 598409a21f4c Slides/Slides2.thy
--- a/Slides/Slides2.thy	Sat Dec 22 14:50:29 2012 +0000
+++ b/Slides/Slides2.thy	Thu Jun 20 13:50:01 2013 -0400
@@ -7,10 +7,12 @@
   set ("_") and
   Cons  ("_::/_" [66,65] 65) 
 
+(*
 ML {*
   open Printer;
   show_question_marks_default := false;
   *}
+*)
 
 notation (latex output)
   Cons ("_::_" [78,77] 73) and