diff -r 438703674711 -r 321e220a6baa ProgTutorial/Parsing.thy --- 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