--- a/ProgTutorial/Parsing.thy	Tue May 21 14:37:39 2019 +0200
+++ b/ProgTutorial/Parsing.thy	Tue May 21 16:22:30 2019 +0200
@@ -1124,7 +1124,7 @@
 
    fun setup_proof (thm_name, src) lthy =
      let
-       val text = Input.source_content src
+       val (text, _) = Input.source_content src
        val trm = Code_Runtime.value lthy result_cookie ("", text)
      in
        Proof.theorem NONE (after_qed thm_name) [[(trm, [])]] lthy