# HG changeset patch
# User wenzelm
# Date 1346234865 -7200
# Node ID 44428ea53dc17ad48bef029449488b1c958cffc3
# Parent  0518bf89c7778014e33bbcc9395793b233f9373d
tuned signature;

diff -r 0518bf89c777 -r 44428ea53dc1 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Wed Aug 29 11:48:45 2012 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Aug 29 12:07:45 2012 +0200
@@ -37,7 +37,6 @@
   val print_of: transition -> bool
   val name_of: transition -> string
   val pos_of: transition -> Position.T
-  val str_of: transition -> string
   val name: string -> transition -> transition
   val position: Position.T -> transition -> transition
   val interactive: bool -> transition -> transition
@@ -359,9 +358,8 @@
 fun print_of (Transition {print, ...}) = print;
 fun name_of (Transition {name, ...}) = name;
 fun pos_of (Transition {pos, ...}) = pos;
-fun str_of tr = quote (name_of tr) ^ Position.here (pos_of tr);
 
-fun command_msg msg tr = msg ^ "command " ^ str_of tr;
+fun command_msg msg tr = msg ^ "command " ^ quote (name_of tr) ^ Position.here (pos_of tr);
 fun at_command tr = command_msg "At " tr;
 
 fun type_error tr state =