diff -r aedfdcae39a9 -r 242e81f4d461 ProgTutorial/Solutions.thy
--- a/ProgTutorial/Solutions.thy	Fri Oct 29 13:46:37 2010 +0200
+++ b/ProgTutorial/Solutions.thy	Wed Feb 23 23:55:37 2011 +0000
@@ -83,8 +83,8 @@
 
   @{ML_response [display,gray]
 "let
-  val input1 = (explode \"foo bar\")
-  val input2 = (explode \"foo (*test*) bar (*test*)\")
+  val input1 = (Symbol.explode \"foo bar\")
+  val input2 = (Symbol.explode \"foo (*test*) bar (*test*)\")
 in
   (scan_all input1, scan_all input2)
 end"