# HG changeset patch
# User wenzelm
# Date 1176640312 -7200
# Node ID 077ce0e019fa6a6e318fed9c52fa6de8f3738686
# Parent  fb5e080fa82b54a5be2e60378c6403b579cd201d
load type_infer.ML early;

diff -r fb5e080fa82b -r 077ce0e019fa src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Sun Apr 15 14:31:51 2007 +0200
+++ b/src/Pure/ROOT.ML	Sun Apr 15 14:31:52 2007 +0200
@@ -29,6 +29,7 @@
 use "type.ML";
 use "context.ML";
 use "compress.ML";
+use "type_infer.ML";
 
 (*inner syntax module*)
 use "Syntax/lexicon.ML";
@@ -50,7 +51,6 @@
 structure Mixfix = Hidden;
 structure Printer = Hidden;
 
-use "type_infer.ML";
 use "General/ml_syntax.ML";
 
 (*core of tactical proof system*)