Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned signature;
authorwenzelm
Wed, 29 Aug 2012 12:07:45 +0200
changeset 48993 44428ea53dc1
parent 48992 0518bf89c777
child 48994 c84278efa9d5
tuned signature;
src/Pure/Isar/toplevel.ML file | annotate | diff | comparison | revisions 
--- 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 =
isabelle