# 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";