# HG changeset patch
# User wenzelm
# Date 1345470190 -7200
# Node ID 034df7b057593c48a004a28d854174b128a5693b
# Parent  9824fd676bf40100e520247bf1c25dddfd406af7
tuned comment;

diff -r 9824fd676bf4 -r 034df7b05759 src/Pure/General/path.ML
--- a/src/Pure/General/path.ML	Mon Aug 20 14:23:20 2012 +0200
+++ b/src/Pure/General/path.ML	Mon Aug 20 15:43:10 2012 +0200
@@ -190,7 +190,7 @@
 val expand = rep #> maps eval #> norm #> Path;
 
 
-(* source position -- with smart replacement ISABELLE_HOME *)
+(* source position -- with smart replacement of ISABELLE_HOME *)
 
 val isabelle_home = explode_path "~~";