src/Pure/Isar/toplevel.ML
changeset 48992 0518bf89c777
parent 48772 e46cd0d26481
child 48993 44428ea53dc1
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Aug 29 11:31:07 2012 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Aug 29 11:48:45 2012 +0200
     1.3 @@ -189,8 +189,8 @@
     1.4    | _ => raise UNDEF);
     1.5  
     1.6  fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy
     1.7 -  | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.str_of pos)
     1.8 -  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.str_of pos);
     1.9 +  | end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos)
    1.10 +  | end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos);
    1.11  
    1.12  
    1.13  (* print state *)
    1.14 @@ -359,7 +359,7 @@
    1.15  fun print_of (Transition {print, ...}) = print;
    1.16  fun name_of (Transition {name, ...}) = name;
    1.17  fun pos_of (Transition {pos, ...}) = pos;
    1.18 -fun str_of tr = quote (name_of tr) ^ Position.str_of (pos_of tr);
    1.19 +fun str_of tr = quote (name_of tr) ^ Position.here (pos_of tr);
    1.20  
    1.21  fun command_msg msg tr = msg ^ "command " ^ str_of tr;
    1.22  fun at_command tr = command_msg "At " tr;