src/HOL/Tools/watcher.ML
changeset 25551 87d89b0f847a
parent 25414 3326bd7ecd48
child 26928 ca87aff1ad2d
     1.1 --- a/src/HOL/Tools/watcher.ML	Thu Dec 06 00:21:28 2007 +0100
     1.2 +++ b/src/HOL/Tools/watcher.ML	Thu Dec 06 00:21:30 2007 +0100
     1.3 @@ -364,7 +364,7 @@
     1.4        val outlines = 
     1.5  	case split_lines s of
     1.6  	    [] => ["Received bad string: " ^ s]
     1.7 -	  | line::lines => ["  Try this command:", (*Markup.enclose Markup.sendback*) line, ""]
     1.8 +	  | line::lines => ["  Try this command:", (*Markup.markup Markup.sendback*) line, ""]
     1.9  	                   @ lines
    1.10    in priority (cat_lines (sgline::sgtx::outlines)) end;
    1.11