changeset 41944 | b97091ae583a |
parent 41887 | ececcbd08d35 |
child 42003 | 6e45dc518ebb |
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Sun Mar 13 15:16:37 2011 +0100 +++ b/src/HOL/Boogie/Tools/boogie_commands.ML Sun Mar 13 16:01:00 2011 +0100 @@ -18,7 +18,7 @@ let val ext = "b2i" fun check_ext path = snd (Path.split_ext path) = ext orelse - error ("Bad file ending of file " ^ quote (Path.implode path) ^ ", " ^ + error ("Bad file ending of file " ^ Path.print path ^ ", " ^ "expected file ending " ^ quote ext) val base_path = Path.explode base_name |> tap check_ext