diff -r 95b42288294e -r 438703674711 ProgTutorial/Base.thy
--- a/ProgTutorial/Base.thy	Fri May 17 11:21:09 2019 +0200
+++ b/ProgTutorial/Base.thy	Tue May 21 14:37:39 2019 +0200
@@ -3,12 +3,6 @@
         "~~/src/HOL/Library/LaTeXsugar"
 begin
 
-print_ML_antiquotations
-
-text \<open>
-Why is Base not printed?
-@{cite "isa-imp"}
-\<close>
 notation (latex output)
   Cons ("_ # _" [66,65] 65)
 
@@ -27,10 +21,6 @@
 ML_file "output_tutorial.ML"
 ML_file "antiquote_setup.ML"
 
-
-(*setup {* OutputTutorial.setup *}*) (* Seems to be standard now, we don't need this anymoe *)
 setup \<open>AntiquoteSetup.setup\<close>
 
-print_ML_antiquotations
-
 end
\ No newline at end of file