src/Tools/Code/code_runtime.ML
changeset 41944 b97091ae583a
parent 41486 82c1e348bc18
child 42359 6ca5407863ed
     1.1 --- a/src/Tools/Code/code_runtime.ML	Sun Mar 13 15:16:37 2011 +0100
     1.2 +++ b/src/Tools/Code/code_runtime.ML	Sun Mar 13 16:01:00 2011 +0100
     1.3 @@ -436,7 +436,7 @@
     1.4      val superfluous = subtract (fn ((name1, _), name2) => name1 = name2) definienda ml_names;
     1.5      val _ = if null superfluous then ()
     1.6        else error ("Value binding(s) " ^ commas_quote superfluous
     1.7 -        ^ " found in external file " ^ quote (Path.implode filepath)
     1.8 +        ^ " found in external file " ^ Path.print filepath
     1.9          ^ " not present among the given contants binding(s).");
    1.10      val these_definienda = AList.make (the o AList.lookup (op =) definienda) ml_names;
    1.11      val thy'' = fold add_definiendum these_definienda thy';