diff -r 6103b0eadbf2 -r f7c97e64cc2a ProgTutorial/Package/Ind_Interface.thy --- a/ProgTutorial/Package/Ind_Interface.thy Tue May 14 17:45:13 2019 +0200 +++ b/ProgTutorial/Package/Ind_Interface.thy Thu May 16 19:56:12 2019 +0200 @@ -107,7 +107,7 @@ If we feed into the parser the string that corresponds to our definition of @{term even} and @{term odd} - @{ML_response [display,gray] + @{ML_matchresult [display,gray] "let val input = filtered_input (\"even and odd \" ^