src/Pure/Isar/ROOT.ML

 use "local_theory.ML";
 use "overloading.ML";
 use "locale.ML";
 use "class.ML";
 
+(*complex proof machineries*)
+use "../simplifier.ML";
+
 (*executable theory content*)
 use "code_unit.ML";
 use "code.ML";
 
 (*local theories and specifications*)

 use "isar.ML";
 use "../Thy/thy_edit.ML";
 
 (*theory and proof operations*)
 use "rule_insts.ML";
-use "../simplifier.ML";
 use "../Thy/thm_deps.ML";
 use "find_theorems.ML";
 use "isar_cmd.ML";
 use "isar_syn.ML";