--- a/src/Pure/ROOT.ML Thu Sep 24 13:33:42 2015 +0200
+++ b/src/Pure/ROOT.ML Thu Sep 24 23:33:29 2015 +0200
@@ -170,8 +170,8 @@
use "envir.ML";
use "consts.ML";
use "primitive_defs.ML";
+use "sign.ML";
use "defs.ML";
-use "sign.ML";
use "term_sharing.ML";
use "pattern.ML";
use "unify.ML";