diff -r dfc7b21d0ee9 -r 45e7491bea47 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Dec 07 21:44:13 2006 +0100
+++ b/src/Pure/ROOT.ML	Thu Dec 07 23:16:55 2006 +0100
@@ -55,8 +55,8 @@
 use "variable.ML";
 use "tctical.ML";
 use "search.ML";
+use "tactic.ML";
 use "meta_simplifier.ML";
-use "tactic.ML";
 use "conjunction.ML";
 use "assumption.ML";
 use "goal.ML";