# HG changeset patch
# User wenzelm
# Date 1191509969 -7200
# Node ID 9131433b19bb0d732c15208a073ef9f837410992
# Parent  64cd13299d3902dacb3e9e5bb771b2e7dda8e64b
load variable.ML before conv.ML;

diff -r 64cd13299d39 -r 9131433b19bb src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Oct 04 16:59:28 2007 +0200
+++ b/src/Pure/ROOT.ML	Thu Oct 04 16:59:29 2007 +0200
@@ -64,9 +64,9 @@
 use "pure_thy.ML";
 use "display.ML";
 use "drule.ML";
-use "conv.ML";
 use "morphism.ML";
 use "variable.ML";
+use "conv.ML";
 use "tctical.ML";
 use "search.ML";
 use "tactic.ML";