# HG changeset patch
# User haftmann
# Date 1216056029 -7200
# Node ID db431936de079d055cb4a172596eaf04137c49d3
# Parent  e16f4baa3db6db51fbb5f5f272c6c372aec7e0db
moved bootstrap of simplifier

diff -r e16f4baa3db6 -r db431936de07 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Mon Jul 14 19:20:28 2008 +0200
+++ b/src/Pure/Isar/ROOT.ML	Mon Jul 14 19:20:29 2008 +0200
@@ -56,6 +56,9 @@
 use "locale.ML";
 use "class.ML";
 
+(*complex proof machineries*)
+use "../simplifier.ML";
+
 (*executable theory content*)
 use "code_unit.ML";
 use "code.ML";
@@ -84,7 +87,6 @@
 
 (*theory and proof operations*)
 use "rule_insts.ML";
-use "../simplifier.ML";
 use "../Thy/thm_deps.ML";
 use "find_theorems.ML";
 use "isar_cmd.ML";