src/Pure/Isar/toplevel.ML
changeset 48993 44428ea53dc1
parent 48992 0518bf89c777
child 49010 72808e956879
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Aug 29 11:48:45 2012 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Aug 29 12:07:45 2012 +0200
     1.3 @@ -37,7 +37,6 @@
     1.4    val print_of: transition -> bool
     1.5    val name_of: transition -> string
     1.6    val pos_of: transition -> Position.T
     1.7 -  val str_of: transition -> string
     1.8    val name: string -> transition -> transition
     1.9    val position: Position.T -> transition -> transition
    1.10    val interactive: bool -> transition -> transition
    1.11 @@ -359,9 +358,8 @@
    1.12  fun print_of (Transition {print, ...}) = print;
    1.13  fun name_of (Transition {name, ...}) = name;
    1.14  fun pos_of (Transition {pos, ...}) = pos;
    1.15 -fun str_of tr = quote (name_of tr) ^ Position.here (pos_of tr);
    1.16  
    1.17 -fun command_msg msg tr = msg ^ "command " ^ str_of tr;
    1.18 +fun command_msg msg tr = msg ^ "command " ^ quote (name_of tr) ^ Position.here (pos_of tr);
    1.19  fun at_command tr = command_msg "At " tr;
    1.20  
    1.21  fun type_error tr state =