diff -r a045600f0c98 -r 957c887b89b5 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Fri Nov 21 15:26:22 1997 +0100 +++ b/src/Pure/ROOT.ML Fri Nov 21 15:27:43 1997 +0100 @@ -27,7 +27,7 @@ use "type_infer.ML"; use "type.ML"; use "sign.ML"; -use "sequence.ML"; +use "seq.ML"; use "envir.ML"; use "pattern.ML"; use "unify.ML";