# HG changeset patch # User wenzelm # Date 880201590 -3600 # Node ID c64867c093fbcf812afa587625995da4597638a6 # Parent 8336e8d7a6807ae9de688912698ebab95f9d5036 tuned; diff -r 8336e8d7a680 -r c64867c093fb src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Nov 21 15:47:39 1997 +0100 +++ b/src/Pure/ROOT.ML Sat Nov 22 13:26:30 1997 +0100 @@ -13,6 +13,7 @@ print_depth 1; use "library.ML"; +use "seq.ML"; use "symtab.ML"; use "name_space.ML"; use "term.ML"; @@ -27,7 +28,6 @@ use "type_infer.ML"; use "type.ML"; use "sign.ML"; -use "seq.ML"; use "envir.ML"; use "pattern.ML"; use "unify.ML";