# HG changeset patch
# User wenzelm
# Date 1384626196 -3600
# Node ID 044faa8a80801881358d722b0de9c73ebdce55b9
# Parent  b9d6e7acad38606a513375116c5c2921bfd34992
tuned;

diff -r b9d6e7acad38 -r 044faa8a8080 src/Pure/Thy/thy_load.ML
--- a/src/Pure/Thy/thy_load.ML	Sat Nov 16 18:34:11 2013 +0100
+++ b/src/Pure/Thy/thy_load.ML	Sat Nov 16 19:23:16 2013 +0100
@@ -1,7 +1,7 @@
 (*  Title:      Pure/Thy/thy_load.ML
     Author:     Makarius
 
-Loading files that contribute to a theory.  Global master path for TTY loop.
+Loading files that contribute to a theory.
 *)
 
 signature THY_LOAD =
@@ -122,11 +122,6 @@
     val id = SHA1.digest text;
   in ((full_path, id), text) end;
 
-(*Proof General legacy*)
-fun loaded_files thy =
-  let val {master_dir, provided, ...} = Files.get thy
-  in map (File.full_path master_dir o #1) provided end;
-
 fun loaded_files_current thy =
   #provided (Files.get thy) |>
     forall (fn (src_path, id) =>
@@ -134,6 +129,11 @@
         NONE => false
       | SOME ((_, id'), _) => id = id'));
 
+(*Proof General legacy*)
+fun loaded_files thy =
+  let val {master_dir, provided, ...} = Files.get thy
+  in map (File.full_path master_dir o #1) provided end;
+
 
 (* load_thy *)