tuned -- more standard operations;

--- a/src/Pure/Thy/present.ML	Mon Mar 07 21:09:28 2016 +0100
+++ b/src/Pure/Thy/present.ML	Mon Mar 07 21:33:41 2016 +0100
@@ -35,7 +35,7 @@
 val doc_indexN = "session";
 val session_graph_path = Path.basic "session_graph.pdf";
 
-fun show_path path = Path.implode (Path.expand (Path.append (File.pwd ()) path));
+fun show_path path = Path.implode (Path.expand (File.full_path Path.current path));
 
 
 

--- a/src/Tools/Code/code_target.ML	Mon Mar 07 21:09:28 2016 +0100
+++ b/src/Tools/Code/code_target.ML	Mon Mar 07 21:33:41 2016 +0100
@@ -348,9 +348,8 @@
 fun assert_module_name "" = error "Empty module name not allowed here"
   | assert_module_name module_name = module_name;
 
-fun using_master_directory ctxt =
-  Option.map (Path.append (File.pwd ()) o
-    Path.append (Resources.master_directory (Proof_Context.theory_of ctxt)));
+val using_master_directory =
+  Option.map o File.full_path o Resources.master_directory o Proof_Context.theory_of;
 
 in