# HG changeset patch # User wenzelm # Date 1147102805 -7200 # Node ID d42149a01a0111b033d4f09f41803e4a26c30f8a # Parent 846f0d5bfc832ba40ca4d83931ac6ec287ebfe52 tuned; diff -r 846f0d5bfc83 -r d42149a01a01 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Mon May 08 12:23:57 2006 +0200 +++ b/src/Pure/ROOT.ML Mon May 08 17:40:05 2006 +0200 @@ -43,9 +43,9 @@ use "theory.ML"; use "proofterm.ML"; use "thm.ML"; -use "display.ML"; use "fact_index.ML"; use "pure_thy.ML"; +use "display.ML"; use "drule.ML"; use "tctical.ML"; use "search.ML";