
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 \" ^  




